Modeling Concurrency in Dafny
Modeling Concurrency in Dafny
复制标题
在 Dafny 中建模并发
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
K. Leino
中科院分区：
文献类型：
--
作者：
K. Leino
这篇文章给出了一个关于如何使用Dafny语言和验证器来建模并发系统的教程。运行的例子是一个简单的互斥票据系统。在公平调度器的假设下，安全性和活跃性都得到了验证。
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.