Project Yin-Yang for SMT Solver Testing

Team

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 [1] and type-aware operator mutation [2]. 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,000+ bugs in Z3 and CVC4, the two state-of-the-art SMT solvers.

We have maintained our continuous, extensive effort in stress-testing Z3 and CVC4 to benefit the SMT solver developer, user, and research communities:

[Summary: 1103 (total) / 703 (fixed)]

[Z3 bugs: 829 (total) / 553 (fixed)]
[CVC4 bugs: 274 (total) / 150 (fixed)]

[Bugs in default mode (Z3): 540 (total) / 386 (fixed)]
[Bugs in default mode (CVC4): 128 (total) / 74 (fixed)]

[Soundness bugs (Z3): 259 (total) / 150 (fixed)]
[Soundness bugs (CVC4): 37 (total) / 25 (fixed)]

Report links: Semantic Fusion (link), Type-aware Operator Mutation (link)

Please follow us on twitter @testsmt for important project developments and regular tweets about interesting bugs in Z3 and CVC4.

Publications

  1. Validating SMT Solvers via Semantic Fusion.
    Dominik Winterer*, Chengyu Zhang* and Zhendong Su
    In Proceedings of PLDI 2020, London, UK, June 2020.
    * Both authors contributed equally to this work.

    Distinguished Paper Award

    [slides | video abstract | talk video]

  2. On the Unusual Effectiveness of Type-aware Mutations for Testing SMT Solvers.
    Dominik Winterer*, Chengyu Zhang* and Zhendong Su
    In Proceedings of SPLASH/OOPSLA 2020, November 2020. (conditionally accepted)
    * Both authors contributed equally to this work.

    arXiv preprint: CoRR, abs/2004.08799, April 2020.


last modified: 2020.08.05