Project Yin-Yang



Introduction

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. Our tools have demonstrated their remarkable effectiveness by having already found 1,500+ bugs in Z3 and CVC4/5, the two state-of-the-art SMT solvers.

Results

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

Yin-Yang project has found    (total) /    (fixed) bugs.

[Z3 bugs: 1199 (total) / 889 (fixed)]
[CVC4/5 bugs: 465 (total) / 354 (fixed)]

[Bugs in default mode (Z3): 709 (total) / 532 (fixed)]
[Bugs in default mode (CVC4/5): 243 (total) / 182 (fixed)]

[Soundness bugs (Z3): 386 (total) / 256 (fixed)]
[Soundness bugs (CVC4/5): 77 (total) / 68 (fixed)]

[Incompleteness bugs (Z3): 13 (total) / 8 (fixed)]
[Incompleteness bugs (CVC4/5): 18 (total) / 11 (fixed)]

Semantic Fusion (report links)
Type-aware Operator Mutation (report links)
Generative Type-aware Mutation (report links)
Weakening and Strengthening (report links)

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

Tools & Publications

Tools

yinyang: https://github.com/testsmt/yinyang

Publications

[1] Validating SMT Solvers via Semantic Fusion.
[slides | abstract video | talk video]
Dominik Winterer*, Chengyu Zhang* and Zhendong Su
In Proceedings of PLDI 2020, London, UK, June 2020.
* Both authors contributed equally to this work.
    PLDI Distinguished Paper Award
[2] On the Unusual Effectiveness of Type-aware Operator Mutations for Testing SMT Solvers.
[slides | abstract video | talk video]
Dominik Winterer*, Chengyu Zhang* and Zhendong Su
In Proceedings of SPLASH/OOPSLA 2020, November 2020.
* Both authors contributed equally to this work.
[3] Generative Type-Aware Mutation for Testing SMT Solvers.
[talk video]
Jiwon Park*, Dominik Winterer*, Chengyu Zhang and Zhendong Su
In Proceedings of SPLASH/OOPSLA 2021, October 2021
* Both authors contributed equally to this work.
[4] Finding and Understanding Incompleteness Bugs in SMT Solvers.
Mauro Bringolf, Dominik Winterer and Zhendong Su
In Proceedings of ASE 2022, October 2022

Contributors




Acknowledgments

This project is partially supported by an Amazon Research Award (Fall '21). We are also grateful to Google for an open source peers bonus.






last modified: 2022.09.29