This article gives a tutorial on how the Dafny language and verifier can be used to model a concurrent system. The running example is a simple ticket system for mutual exclusion. Both safety and, under the assumption of a fair scheduler, liveness are verified.
CITATION STYLE
Leino, K. R. M. (2018). Modeling concurrency in dafny. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11174 LNCS, pp. 115–142). Springer Verlag. https://doi.org/10.1007/978-3-030-02928-9_4
Mendeley helps you to discover research relevant for your work.