一句话：提出惰性顺序化，将有界多线程 C 程序转为串行程序，复用 BMC 高效验证并发。
有界模型检测（BMC）在程序分析中很成功，但并发仍是难题。本文针对使用 POSIX 线程的顺序一致命令式程序，提出一种 BMC 新方法：先将多线程程序转换为非确定性顺序程序，在给定轮次数界下保持所有轮转调度的可达性；随后复用高性能 BMC 工具作为后端。该转换刻意控制内存开销与非确定性来源，从而生成紧凑的 SAT/SMT 公式。作者给出转换细节并证明正确性，基于 CSeq 框架实现 Lazy-CSeq，并进行详细评估与比较。该工具在 SV-COMP 2014–2021 并发类别获多枚金/银牌，并能发现其他技术（包括测试）未能发现的错误。
Bounded verification techniques such as bounded model checking (BMC) have successfully been used for many practical program analysis problems, but concurrency still poses a challenge. Here, we describe a new approach to BMC of sequentially consistent imperative programs that use POSIX threads. We first translate the multi-threaded program into a nondeterministic sequential program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. We then reuse existing high-performance BMC tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so it produces tight SAT/SMT formulae, and is thus very effective in practice: Our Lazy-CSeq tool implementing this translation for the C programming language won several gold and silver medals in the concurrency category of the Software Verification Competitions (SV-COMP) 2014–2021 and was able to find errors in programs where all other techniques (including testing) failed. In this article, we give a detailed description of our translation and prove its correctness, sketch its implementation using the CSeq framework, and report on a detailed evaluation and comparison of our approach.
@article{paperbot1203,
title = {Bounded Verification of Multi-threaded Programs via Lazy Sequentialization},
author = {Omar Inverso and Ermenegildo Tomasco and Bernd Fischer and Salvatore La Torre and Gennaro Parlato},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {1},
year = {2021},
doi = {10.1145/3478536}
}