Modular SMT proofs for fast reflexive checking inside Coq

DOI10.1007/978-3-642-25379-9_13MaRDI QIDQ3100210zbMATH OpenOpenAlexFDO

Authors Frédéric Besson, Pierre Cornilleau, David Pichardie

Publication date 22 November 2011

Published in Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-25379-9_13

Mathematics Subject Classification ID

Recommendations

• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Rocket-Fast Proof Checking for SMT Solvers
• Extending Coq with Imperative Features and Its Application to SAT Verification
• SMT proof checking using a logical framework

Cites work

• scientific article; zbMATH DE number 1614685 (Why is no real title available?)
• scientific article; zbMATH DE number 1234104 (Why is no real title available?)
• scientific article; zbMATH DE number 2090318 (Why is no real title available?)
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
• A compiled implementation of strong reduction
• Automated Deduction – CADE-20
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• Efficiently checking propositional refutations in HOL theorem provers
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Fast LCF-Style Proof Reconstruction for Z3
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Justifying equality
• Simplification by Cooperating Decision Procedures
• Simplify: a theorem prover for program checking
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Term Rewriting and Applications
• Theorem Proving in Higher Order Logics
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(8)

• A solver for arrays with concatenation
• Extending Coq with Imperative Features and Its Application to SAT Verification
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Tactics for Reasoning Modulo AC in Coq
• scientific article; zbMATH DE number 1301729 (Why is no real title available?)
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Extensible and efficient automation through reflective tactics
• Fast Reflexive Arithmetic Tactics the Linear Case and Beyond

Describes a project that uses

Uses Software

• Gandalf
• CVC Lite
• veriT
• HOL Light
• SIMPLIFY
• z3
• cvc3
• Metis
• Coq

This page was built for publication: Modular SMT proofs for fast reflexive checking inside Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3100210)