Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
From MaRDI portal
Publication:606999
DOI10.1016/j.tcs.2010.09.014zbMath1208.68205OpenAlexW1991066194MaRDI QIDQ606999
Publication date: 19 November 2010
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2010.09.014
Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
versat: A Verified Modern SAT Solver ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Strategyproof social choice when preferences and outcomes may contain ties ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ Efficient, verified checking of propositional proofs ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ SMT proof checking using a logical framework ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points ⋮ Unnamed Item ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ A flexible proof format for SAT solver-elaborator communication ⋮ Efficient verified (UN)SAT certificate checking ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers ⋮ Animating the Formalised Semantics of a Java-Like Language ⋮ SAT Solver Verification
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Formalization and implementation of modern SAT solvers
- Isabelle/HOL. A proof assistant for higher-order logic
- Towards mechanical metamathematics
- Solving SAT and SAT Modulo Theories
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Imperative Functional Programming with Isabelle/HOL
- GRASP: a search algorithm for propositional satisfiability
- The Mechanical Verification of a DPLL-Based Satisfiability Solver
- SATO: An efficient propositional prover
- Theory and Applications of Satisfiability Testing
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- The complexity of theorem-proving procedures
This page was built for publication: Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
