文件名称：dafny-jrnl:将Perennial和Dafny与经过验证的期刊相结合
文件大小：99KB
文件格式：ZIP
更新时间：2024-04-06 01:48:42
verification dafny Dafny
达芙妮 使用顺序证明来验证崩溃安全的并发代码。 目标是将goose-nfsd的经过验证的日记与Dafny中的顺序验证相联系：该想法是该日记应该使顺序推理成为顺序，在这种情况下，我们可以在执行生产证明系统（如Dafny）时仅使用顺序推理来证明应用程序正确Perennial中复杂的并发和崩溃安全推理。 状态 编译中 运行make verify验证所有内容，并make compile以将文件系统和bank示例编译为Go（生成的代码进入dafnygen/ ）。 您需要Dafny 3： 在Arch Linux上，您可以从AUR获取dafny-bin 在macOS上使用brew install dafny 对于其他系统，最简单的解决方案是从下载一个二进制发行版，将其解压缩，然后将其添加到您的$ PATH中（这是我们在CI中要做的，在Ubuntu 20.04上运行）。 编译还依赖于goimp