versat: A Verified Modern SAT Solver

DOI10.1007/978-3-642-27940-9_24MaRDI QIDQ2891429zbMATH OpenOpenAlexFDO

Authors Duckki Oe, Aaron Stump, Corey Oliver, Kevin Clancy

Publication date 15 June 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-27940-9_24

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)

Recommendations

• A verified SAT solver framework with learn, forget, restart, and incrementality
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Formalization and implementation of modern SAT solvers
• Anatomy and empirical evaluation of modern SAT solvers
• Empirical study of the anatomy of modern SAT solvers
• Solving quantified verification conditions using satisfiability modulo theories

Cites work

• Automated testing and debugging of SAT and QBF solvers
• Bounded model checking using satisfiability solving
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Garbage collection: Java application servers' Achilles heel
• Rocket-Fast Proof Checking for SMT Solvers
• The mechanical verification of a DPLL-based satisfiability solver

Cited in

(20)

• A verified SAT solver framework with learn, forget, restart, and incrementality
• Efficient, verified checking of propositional proofs
• A flexible proof format for SAT solver-elaborator communication
• Verifying the conversion into CNF in dafny
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• A verified SAT solver framework with learn, forget, restart, and incrementality
• SpyBug: automated bug detection in the configuration space of SAT solvers
• MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
• An expressive model for instance decomposition based parallel SAT solvers
• A flexible proof format for SAT solver-elaborator communication
• The mechanical verification of a DPLL-based satisfiability solver
• Efficient verified (UN)SAT certificate checking
• Formalized proof systems for propositional logic
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Verified verifying: SMT-LIB for strings in Isabelle
• A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
• \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
• Verified AIG algorithms in ACL2
• Certainty in formalising SMT-LIB for strings in Isabelle
• Formal verification of the empty hexagon number

Describes a project that uses

Uses Software

• Coq
• HOL Light
• versat
• veriT
• CVC Lite
• seL4

This page was built for publication: versat: A Verified Modern SAT Solver

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2891429)