Write a Blog >>
PPoPP 2022
Sat 2 - Wed 6 April 2022
Tue 5 Apr 2022 11:55 - 12:10 - Session 5 Chair(s): Wenwen Wang

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 \emph{ConcurrencySafety} category of \emph{SV-COMP} 2019. Experimental results show promising improvements attributed to our approach.

Tue 5 Apr

Displayed time zone: Eastern Time (US & Canada) change

11:40 - 12:25
Session 5Main Conference
Chair(s): Wenwen Wang University of Georgia
11:40
15m
Talk
Vapro: Performance Variance Detection and Diagnosis for Production-Run Parallel Applications
Main Conference
Liyan Zheng Tsinghua University, Jidong Zhai Tsinghua University, Xiongchao Tang Sangfor Technologies Inc. and Tsinghua University, Haojie Wang Tsinghua University, Teng Yu Tsinghua University, Yuyang Jin Tsinghua University, Shuaiwen Leon Song University of Sydney, Wenguang Chen Tsinghua University
11:55
15m
Talk
Interference Relation-Guided SMT Solving for Multi-Threaded Program Verification
Main Conference
Hongyu Fan Tsinghua University, Weiting Liu Tsinghua University, Fei He Tsinghua University
12:10
15m
Talk
PerFlow: A Domain Specific Framework for Automatic Performance Analysis of Parallel Applications
Main Conference
Yuyang Jin Tsinghua University, Haojie Wang Tsinghua University, Runxin Zhong Tsinghua University, Chen Zhang Tsinghua University, Jidong Zhai Tsinghua University