文件名称：dafny-nfsd:将Perennial和Dafny与经过验证的期刊相结合
文件大小：98KB
文件格式：ZIP
更新时间：2024-04-10 01:13:47
verification dafny Dafny
dafny-nfsd 使用顺序证明来验证崩溃安全的并发文件系统。目标是将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上运行）。