一句话：提出条件插值并与CEGAR结合，通过剪除不可行分支和缩短插值路径提升并发程序验证效率。
大规模真实程序的高效验证仍受状态空间爆炸问题困扰，而并发程序中线程交替进一步加剧了该问题。本文将Craig插值的一种应用——条件插值——与基于CEGAR的方法结合，用于缩减并发任务的状态空间。具体而言，论文形式化了条件插值，以限定可达状态区域，从而剪除不可行的条件分支；同时利用生成的条件插值式缩短插值路径，显著减少验证耗时。作者在开源软件模型检测器上实现了所提方法，实验结果表明条件插值能够有效提升并发任务的验证效率。
Due to the state-space explosion problem, efficient verification of real-world programs in large scale is still a big challenge. Particularly, thread alternation makes the verification of concurrent programs much more difficult since it aggravates this problem. In this paper, an application of Craig interpolation, namely conditional interpolation, is proposed to work together with CEGAR-based approach to reduce the state-space of concurrent tasks. Specifically, conditional interpolation is formalized to confine the reachable region of states so that infeasible conditional branches could be pruned. Furthermore, the generated conditional interpolants are utilized to shorten the interpolation paths, which makes the time consumed for verification significantly reduced. We have implemented the proposed approach on top of an open-source software model checker. Empirical results show that the conditional interpolation is effective in improving the verification efficiency of concurrent tasks.
DOI 原文 ·
@inproceedings{paperbot6310,
title = {Conditional interpolation: making concurrent program verification more effective},
author = {Jie Su and Cong Tian and Zhenhua Duan},
booktitle = {FSE},
year = {2021},
doi = {10.1145/3468264.3468602}
}