Abstract
Satisfiability Modulo Theories (SMT) solvers are a critical component of
many formal methods applications, including for software verification
and security analysis. Their soundness is of the utmost importance.
While SMT solvers are highly complex systems, some modern SMT solvers
now are capable of generating externally checkable proofs. This talk
gives the current state of proofs in the SMT solver cvc5. We introduce
our current work on AletheLF, a logical framework for proofs generated
by cvc5. AletheLF is a logical framework loosely based on the SMT-LIB
version 3.0 language. It combines the benefits of several previous proof
efforts, including a clean syntax, extensibility and integration with
other proof formats like DRAT via the use of oracles. We present an
evaluation of AletheLF, showing the viability of performant proof
generation and checking for SMT. We mention initial work on a second
generation of this logical framework for handling new challenges for
proofs in SMT.
Bio
Andrew Reynolds is a research scientist at the University of Iowa, a
visiting scholar at Amazon Web Services (AWS), 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.