Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
Burak Ekici (The University of Iowa), Guy Katz (New York University),, Chantal Keller (LRI, Univ. Paris-Sud), Alain Mebsout (The University of, Iowa), Andrew J. Reynolds (The University of Iowa), Cesare Tinelli (The, University of Iowa)
TL;DR
This paper discusses progress on SMTCoq, a tool that verifies external SAT/SMT solver results within Coq, enhancing proof automation and safety, with ongoing extensions to support additional solvers and theories.
Contribution
It extends SMTCoq's capabilities to support more solvers and theories, improving proof checking and automation in Coq with a correct, extendable framework.
Findings
Supports zChaff and veriT solvers for specific theories
Ensures safe verification of external solver answers
Work in progress to include CVC4 and bit vectors
Abstract
This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's automation using such solvers, in a safe way. Currently supporting the SAT solver zChaff, and the SMT solver veriT for the combination of the theories of congruence closure and linear integer arithmetic, SMTCoq is meant to be extendable with a reasonable amount of effort: we present work in progress to support the SMT solver CVC4 and the theory of bit vectors.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDigital Rights Management and Security