将虹膜引入验证软件工具链
摘要：使用分离逻辑证明C程序正确性的Verified Software Toolchain (VST) 是一个系统。通过连接到经过验证的编译器CompCert，它能够为我们可以编译和运行的真实C代码提供最可靠的正确性保证。VST从一开始就包括并发性，形式上是通过对锁不变量进行推理。但是，自那时以来，并发分离逻辑 (CSL) 已经取得了重大进展。在本文中，我们描述了将来自Iris的最新机械化CSL的发展融入VST的努力。Iris的一些特性（幽灵状态和不变量）从零开始重新实现在VST中；其他特性（Iris Proof Mode）从Iris开发中引入；还有一些特性（用于原子操作的证明规则）则进行了公理化，希望它们将在将来的版本中成为基础。结果是，该系统能够证明在C中实现的复杂并发程序的正确性，具有细粒度的锁定和非阻塞的原子操作，根据使用的特性提供不同的可靠性保证。
作者：William Mansky
论文ID：2207.06574
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-07-18