Equality Reasoning in CVC5
2024-05-16
In the past several decades, Satisfiability Modulo Theories (SMT) solvers have become vital backends in many formal methods applications. At a high level, an SMT solver combines a propositional (SAT) solver with several theory solvers. Due to the diversity of applications, SMT solvers have been extended to support a growing number of theories. This talk will overview some of the key design decisions behind theory solvers in the SMT solver cvc5. In particular, several theory solvers can be viewed as extensions of the congruence closure algorithm, where dedicated callbacks are used to inject theory-specific inferences. I will discuss key optimizations to this design and how these solvers fit into the overall architecture of cvc5.
Speaker
Andrew Reynolds is a research scientist at the University of Iowa, and one of the lead developers of the state-of-the-art Satisfiability Modulo Theories (SMT) solver cvc5. His research spans several aspects of SMT, including approaches for unbounded strings and regular expressions, syntax-guided synthesis conjectures, and first-order theorem proving. His work in cvc5 (and its predecessor CVC4) has entered numerous competitions and has received awards spanning several automated reasoning communities, including SMT, automated theorem proving, and syntax-guided synthesis. His research has been used in several large-scale and industrial applications in interactive theorem proving, verification, and security.