Better SMT Proofs for Certifying Compliance and Correctness

Explore a comprehensive lecture on improving SMT (Satisfiability Modulo Theories) proofs for certifying compliance and correctness. Delve into the complete redesign and extension of cvc5's proof-production infrastructure, presented by Haniel Barbosa from Universidade Federal de Minas Gerais. Discover how machine-checkable certificates address trust issues in SMT solvers by decoupling result confidence from solver implementation. Learn about the enhanced integration of cvc5 into proof assistants like Lean and Isabelle/HOL, as well as its applications in industrial settings. Gain insights into the challenges of trusting complex SMT solver codebases and the solutions offered by logical reasoning proofs. Recorded at IPAM's Machine Assisted Proofs Workshop at UCLA, this 59-minute talk provides valuable knowledge for researchers and practitioners in the field of automated reasoning and formal verification.