Extending Coq with Imperative Features and Its Application to SAT Verification
From MaRDI portal
Publication:5747643
DOI10.1007/978-3-642-14052-5_8zbMath1291.68318OpenAlexW1795725592MaRDI QIDQ5747643
Arnaud Spiwack, Michaël Armand, Benjamin Grégoire, 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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
versat: A Verified Modern SAT Solver ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ Enabling floating-point arithmetic in the Coq proof assistant ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ The \textsc{MetaCoq} project ⋮ Primitive Floats in Coq ⋮ A light-weight integration of automated and interactive theorem proving ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ Type classes for mathematics in type theory ⋮ A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ Formal Proofs for Nonlinear Optimization ⋮ A framework for the verification of certifying computations ⋮ Implementing and reasoning about hash-consed data structures in Coq
Uses Software
This page was built for publication: Extending Coq with Imperative Features and Its Application to SAT Verification
