Extending Coq with Imperative Features and Its Application to SAT Verification
From MaRDI portal
Publication:5747643
DOI10.1007/978-3-642-14052-5_8zbMATH Open1291.68318OpenAlexW1795725592MaRDI QIDQ5747643FDOQ5747643
Authors: Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry 
Publication date: 14 September 2010
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00502496v2/file/fastcoq.pdf
Recommendations
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Formalizing implicative algebras in Coq
- scientific article; zbMATH DE number 1927413
- Verifying object-oriented programs with higher-order separation logic in Coq
- Modular SMT proofs for fast reflexive checking inside Coq
- Saturated semantics for coalgebraic logic programming
- scientific article; zbMATH DE number 1301729
- Formal verification of cP systems using Coq
- A Coq library for verification of concurrent programs
- From proposition to program. Embedding the refinement calculus in Coq
Cited In (18)
- Formal Proofs for Nonlinear Optimization
- The \textsc{MetaCoq} project
- Type classes for mathematics in type theory
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Mtac: A monad for typed tactic programming in Coq
- Automated Deduction – CADE-20
- A framework for the verification of certifying computations
- Primitive Floats in Coq
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Enabling floating-point arithmetic in the Coq proof assistant
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Computer Certified Efficient Exact Reals in Coq
- Implementing and reasoning about hash-consed data structures in Coq
- Modular SMT proofs for fast reflexive checking inside Coq
- A light-weight integration of automated and interactive theorem proving
- Title not available (Why is that?)
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- versat: A Verified Modern SAT Solver
Uses Software
This page was built for publication: Extending Coq with Imperative Features and Its Application to SAT Verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747643)
