Viewing profile — inaseer

Have you looked at model-based testing? One way to think of it as property-based testing for stateful system, though that's underselling it a little. It's surprisingly easy to come…

There are really two separate concerns here. The first is that some effect happens asynchronously, potentially interleaved with other operations. Whether a client observes completi…

Property-based testing and model-based testing are closely related. Both ask the developer to state the expected behavior of a system (whether you call it a property, invariant, mo…

I've been working on a framework for writing executable specs in .NET called Accordant, developed at Microsoft and open sourced recently. Github: https://github.com/microsoft/accor…

Soon!

Yes, I understand why you made these design decisions. And I also agree that sticking to JS/TS keeps things simple (for humans, and LLMs). I generally default to the s and s' way o…

Bombadil takes a fresh approach to UI testing I haven't seen before: online monitoring through LTL formulas. Unlike model-checking (say by TLC), LTL formulas over here unfold in lo…

+1. We have used Coyote/P# not just for model checking an abstract design (which no doubt is very useful) but testing real implementations of production services at Microsoft.

Microsoft Azure Storage | Seattle, WA | Onsite or Remote (US only) Our team in Azure Storage is working on applying automated reasoning and validation techniques to scalably genera…

My team used Coyote to test their distributed service against network race conditions. It requires a little bit of setup to ensure all components that typically run on separate mac…

TLA+ and Coyote pair quite well actually. Verifying the high level design in TLA+ while checking subtle bugs as you translate that design to an implemention.

Check out Coyote (which is an evolution of P) and allows you to "model check" .NET code to find hard to find race condition-y bugs in your implementation. We have used it very succ…

Coyote (concurrency exploration tool for .NET programs) can be used to do something "similar". My team often writes tests which set up focused concurrency between different APIs, t…

Visualizations do help a lot when model checkers and concurrency schedule exploration tools like Coyote find bugs. Coyote include the ability to visualize the traces if you express…

Loom's style of exploration (and that of aws shuttle mentioned below) can be quite effective. Coyote is the equivalent library in the .NET world (formerly known as P#) and comes wi…

There has been a bunch of content on Coyote shared before as well but the quality of animations and how they explain how it works under the hood in this introduction was excellent.…

Hi HN, The tweet links to a couple of tutorials showing how to test an extremely simple CRUD service using Coyote to find concurrency bugs. Developers write simple unit tests whose…

Shameless plug: http://imnaseer.net/paxos-from-the-ground-up.html I worked on an explanation of Paxos where we start with a simple but incorrect implementation of the protocol. The…

Concurrency is hard - this was a great investigation into the bug using TLA+ by the author which suggested simplifications to the code in addition to the bug fix. This reminded me …

This is a fair call-out. I'll like to share a counter-example where we 'model check' our real-world service written in C# with pretty decent effectiveness. As you rightly call out,…

This is a good callout. P language evolved into the P# framework (as opposed to a language) which then evolved into Coyote ( https://microsoft.github.io/coyote/ ) Coyote allows dev…

Neat to learn about thread sanitizer. It sounds similar to another tool from Microsoft Research called Torch ( https://www.microsoft.com/en-us/research/project/torch/ ) which autom…