SMT solvers can be hard to trust, since it generally means assuming their large and complex codebases do not contain bugs leading to wrong results. Machine-checkable certificates, via proofs of the logical reasoning the solver has performed, address this issue by decoupling confidence in the results from the solver’s implementation. In this talk we will describe the complete redesign and extension of cvc5's (a state-of-the-art SMT solver) proof-production infrastructure, thus enabling its better integration into proof assistants, such as Lean and Isabelle/HOL, and industrial settings.
Copyright. All Rights Reserved.