Modular SMT proofs for fast reflexive checking inside Coq

DOI10.1007/978-3-642-25379-9_13zbMATH Open1350.68224OpenAlexW92909155MaRDI QIDQ3100210FDOQ3100210

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

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

Mathematics Subject Classification ID

Cites Work

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

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
• Title not available (Why is that?)
• 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

Uses Software

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

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)