On SMT Solving for Multi-threaded Program Verification
COM1 Level 3
MR1, COM1-03-19 and via Zoom (Hybrid)
Abstract:
Verifying multi-threaded programs is difficult because of the vast number of thread interleavings. Partial orders (called happens-before orders) can help with verification because they can represent many thread interleavings concisely. It is thus desired to efficiently handle happens-before order constraints for SMT-based multi-threaded program verification.
In this talk, I will report our recent work in this research line. We formalize a new ordering consistency theory for multi-threaded program verification that is applicable under various memory models (including sequential consistency, TSO and PSO). We develop two solvers for ordering consistency theory. The first solver checks consistency incrementally, generates minimal conflict clauses, and includes a custom propagation procedure. The second solver, based on preventive reasoning, has no requirement for consistency checking and conflict clause generation, and is thus more efficient. We implement our approaches in a prototype tool called Deagle, which won ConcurrencySafety track in SV-COMP 2022.
Biodata:
Dr. Fei He is an associate professor at the School of Software of Tsinghua University. He received the PhD. degree from Tsinghua University in 2008. His research interests include model checking, program verification and automated logic reasoning. He has published over 70 papers in academic journals and international conferences. He is currently on the editor board of "Theory of Computing Systems" and "Frontiers of Computer Science". He has served as the PC member for many formal methods conferences, including ICSE, ESEC/FSE, CONCUR, FMCAD, SAT, ATVA, APLAS, ICECCS, SETTA, etc.