Extending Coq with Imperative Features and Its Application to SAT Verification
From MaRDI portal
Publication:5747643
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
- A framework for the verification of certifying computations
- Automated Deduction – CADE-20
- 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
- Mtac: a monad for typed tactic programming in Coq
- A light-weight integration of automated and interactive theorem proving
- scientific article; zbMATH DE number 1696436 (Why is no real title available?)
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- versat: A Verified Modern SAT Solver
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)
