Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL

DOI10.1016/J.TCS.2010.09.014zbMath1208.68205OpenAlexW1991066194MaRDI QIDQ606999

Filip Marić

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

zbMATH Keywords

SAT problemIsabelleDPLL procedureformal program verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (19)

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

• Unnamed Item
• Unnamed Item
• Unnamed Item
• SATO
• OCaml
• Chaff
• BerkMin
• Archive Formal Proofs

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