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
Publications
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.
Tweets by testsmtsolvers
last modified: 2022.09.29
