Post by Informal Systems

We found two liveness bugs in published GWTS pseudocode via simulation and reasoning. Then we used Quint’s new TLC integration to formally verify liveness as a temporal property across the full reachable state space. We get a 27-step lasso counterexample in the original algorithm, and no violations once we include our proposed solution. Linked in comments ↓ #DistributedSystems #FormalMethods #ModelChecking #Quintlang