Better SMT proofs for certifying compliance and correctness

Haniel Barbosa
Universidade Federal de Minas Gerais in Belo Horizonte

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.

Presentation (PDF File)

Back to Machine Assisted Proofs