SMT Solver Testing
Project Goal
Satisfiability Modulo Theory (SMT) solvers are foundational tools for many subareas of computer science, including formal verification, programming languages, and software engineering. Their reliability and robustness are crucial, especially for the safety-critical domains. However, effectively validating SMT solvers has been a longstanding challenge. The goal of Project Yin-Yang is to develop novel, effective, practical methods and techniques to help make SMT solvers more reliable, powerful, and usable. To this end, we have introduced two novel, highly effective techniques for stress-testing SMT solvers: semantic fusion and type-aware operator mutation. The key idea behind semantic fusion is to systematically combine two existing equisatisfiable (i.e., both satisfiable or unsatisfiable) formulas into a new formula that, by construction, preserves satisfiability. Type-aware operator mutation is a simple, general, unusually effective approach for differentially testing SMT solvers by generating diverse type-correct formulas. YinYang and OpFuzz, the realizations of semantic fusion and type-aware operator mutation, have demonstrated their remarkable effectiveness by having already found 1,500+ bugs in Z3 and CVC4, the two state-of-the-art SMT solvers.