Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Wed 17 Jun 2020 14:20 - 14:40 at PLDI Research Papers live stream - Bug Finding Chair(s): Hans-J. Boehm

We introduce Semantic Fusion, a general, effective methodology for validating Satisfiability Modulo Theory (SMT) solvers. Our key idea is to use two existing equisatisfiable (i.e., both satisfiable or unsatisfiable) formulas into a new formula that combines the structures of its ancestors in a novel manner and preserves the satisfiability by construction. This fused formula is then used for validating SMT solvers.

We realized Semantic Fusion as YinYang, a practical SMT solver testing tool. During four months of extensive testing, YinYang has found 45 confirmed, unique bugs in the default arithmetic and string solvers of Z3 and CVC4, the two state-of-the-art SMT solvers. Among these, 41 have already been fixed by the developers. The majority (29/45) of these bugs expose critical soundness issues. Our bug reports and testing effort have been well-appreciated by SMT solver developers.

Wed 17 Jun
Times are displayed in time zone: Pacific Time (US & Canada) change

14:20 - 14:40
Validating SMT Solvers via Semantic Fusion
PLDI Research Papers
Dominik WintererETH Zurich, Switzerland, Chengyu ZhangEast China Normal University, Zhendong SuETH Zurich, Switzerland
14:40 - 15:00
Debugging and Detecting Numerical Errors in Computation with Posits
PLDI Research Papers
Sangeeta ChowdharyRutgers University, USA, Jay P. LimRutgers University, USA, Santosh NagarakatteRutgers University, USA
15:00 - 15:20
SmartTrack: Efficient Predictive Race Detection
PLDI Research Papers
Jake RoemerOhio State University, USA, Kaan GençOhio State University, USA, Michael D. BondOhio State University, USA
15:20 - 15:40
Understanding Memory and Thread Safety Practices and Issues in Real-World Rust Programs
PLDI Research Papers
Boqin QinBeijing University of Posts and Telecommunications, Pennsylvania State University, Yilun ChenPurdue University, USA, Zeming YuPennsylvania State University, USA, Linhai SongPennsylvania State University, USA, Yiying ZhangUniversity of California at San Diego, USA