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 JunDisplayed time zone: Pacific Time (US & Canada) change
14:20 - 15:40 | |||
14:20 20mTalk | Validating SMT Solvers via Semantic Fusion PLDI Research Papers Dominik Winterer ETH Zurich, Switzerland, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich, Switzerland | ||
14:40 20mTalk | Debugging and Detecting Numerical Errors in Computation with Posits PLDI Research Papers Sangeeta Chowdhary Rutgers University, USA, Jay P. Lim Rutgers University, USA, Santosh Nagarakatte Rutgers University, USA | ||
15:00 20mTalk | SmartTrack: Efficient Predictive Race Detection PLDI Research Papers Jake Roemer Ohio State University, USA, Kaan Genç Ohio State University, USA, Michael D. Bond Ohio State University, USA | ||
15:20 20mTalk | Understanding Memory and Thread Safety Practices and Issues in Real-World Rust Programs PLDI Research Papers Boqin Qin Beijing University of Posts and Telecommunications, Pennsylvania State University, Yilun Chen Purdue University, USA, Zeming Yu Pennsylvania State University, USA, Linhai Song Pennsylvania State University, USA, Yiying Zhang University of California at San Diego, USA | ||