testsmt.github.io - Project Yin-Yang for SMT Solver Testing

Description: 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. Ou

Example domain paragraphs

[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)]

Links to testsmt.github.io (2)

wintered.github.io Dominik Winterer
chengyuzhang.com Chengyu Zhang's Homepage