摘要: Concurrent program verification is challenging due to a large number of thread interferences. A popular approach is to encode concurrent programs as SMT formulas and then rely on off-the-shelf SMT solvers to accomplish the verification. In most existing works, an SMT solver is simply treated as the backend. There is little research on improving SMT solving for concurrent program verification.
In this paper, we recognize the characteristics of interference relation in multi-threaded programs and propose a novel approach for utilizing the interference relation in the SMT solving of multi-threaded program verification under various memory models. We show that the backend SMT solver can benefit a lot from the domain knowledge of concurrent programs. We implemented our approach in a prototype tool called Zpre. We compared it with the state-of-the-art Z3 tool on credible benchmarks from the ConcurrencySafety category of SV-COMP 2019. Experimental results show promising improvements attributed to our approach.
个人简介：贺飞，清华大学长聘副教授，博士生导师。主要从事程序验证、模型检验和自动推理的研究。开发了模型检验和软件验证工具，并应用于国家重大安全领域。在包括POPL, CAV, PLDI, OOPSLA, PPoPP, ICSE, ESEC/FSE, ASE等在内的国际重要会议和期刊上发表论文70余篇。现任《Theory of Computing Systems》编委，《Frontiers of Computer Science》青年副主编，曾/现任ICSE, ESEC/FSE, CONCUR, FMCAD, SAT, ATVA, APLAS, ICECCS, SETTA等国际学术会议程序委员会委员。系CCF形式化专委会常务委员，曾获2008年度CCF优秀博士学位论文提名奖、ASE 2018 Distinguished Paper、PPoPP 2022 Best Paper奖等。
