Proofs in cvc5: New Directions with AletheLF

By Andrew J. Reynolds

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.