一句话：提出 Armada 语言与工具，借助 SMT 自动化和可扩展的可靠推理技术，低代价形式验证高性能并发程序。
编写既高性能又安全的并发程序极为困难，而传统形式验证往往代价高昂。Armada 是一个面向并发程序验证的语言与工具：它采用类 C 语言与小步、基于状态机的语义，允许开发者自由选择内存布局与同步原语，以免限制性能优化。为降低验证负担，Armada 借助 SMT 自动化与一组强大的推理技术库，包括 rely-guarantee、TSO 消除、reduction 和指针分析；这些技术均已被证明可靠，且 Armada 可随时间可靠地扩展新的验证策略。作者使用 Armada 验证了五个并发案例研究，并表明所验证代码可达到与未验证代码相当的性能。
Safely writing high-performance concurrent programs is notoriously difficult. To aid developers, we introduce Armada, a language and tool designed to formally verify such programs with relatively little effort. Via a C-like language and a small-step, state-machine-based semantics, Armadagives developers the flexibility to choose arbitrary memory layout and synchronization primitives so that they are never constrained in their pursuit of performance. To reduce developer effort, Armadaleverages SMT-powered automation and a library of powerful reasoning techniques, including rely-guarantee, TSO elimination, reduction, and pointer analysis. All of these techniques are proven sound, and Armadacan be soundly extended with additional strategies over time. Using Armada, we verify five concurrent case studies and show that we can achieve performance equivalent to that of unverified code.
@article{paperbot1615,
title = {Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility},
author = {Jacob R. Lorch and Yixuan Chen and Manos Kapritsos and Haojun Ma and Bryan Parno and Shaz Qadeer and Upamanyu Sharma and James R. Wilcox and Xueyuan Zhao},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {2},
year = {2022},
doi = {10.1145/3502491}
}