PROJECT YIN-YANG FOR SMT SOLVER TESTING

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.

Primary location: London United Kingdom