一句话：提出一致性保持的预防式传播方法，使并发程序验证的 SMT 序理论求解可省略一致性检查与冲突子句生成。
并发程序验证通常用 happens-before 序来建模线程交错行为，其核心是一个专门的序理论求解器，由理论传播、一致性检查和冲突子句生成三部分组成，后两者带来显著开销。本文提出一种预防式（preventive）推理方法：在理论传播过程中自动保持序一致性，使一致性检查与冲突子句生成成为可省略的步骤，从而简化求解器结构并减少冗余推理。作者实现了原型工具，并在可信基准上开展实验，结果表明相比现有最先进的并发程序验证器有显著性能提升。
The happens-before orders have been widely adopted to model thread interleaving behaviors of concurrent programs. A dedicated ordering theory solver, usually composed of theory propagation, consistency checking, and conflict clause generation, plays a central role in concurrent program verification. We propose a novel preventive reasoning approach that automatically preserves the ordering consistency and makes consistency checking and conflict clause generation omissible. We implement our approach in a prototype tool and conduct experiments on credible benchmarks; results reveal a significant improvement over existing state-of-the-art concurrent program verifiers.
@article{paperbot1424,
title = {Consistency-preserving propagation for SMT solving of concurrent program verification},
author = {Zhihang Sun and Hongyu Fan and Fei He},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563321}
}