versat: A Verified Modern SAT Solver

DOI10.1007/978-3-642-27940-9_24zbMath1326.68263OpenAlexW46694604MaRDI QIDQ2891429

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)

Related Items (12)

Verifying the conversion into CNF in dafny ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Efficient, verified checking of propositional proofs ⋮ An Expressive Model for Instance Decomposition Based Parallel SAT Solvers ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Unnamed Item ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Unnamed Item ⋮ 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

Uses Software

• Unnamed Item
• HOL Light
• veriT
• CVC Lite
• versat
• seL4

Cites Work

• Unnamed Item
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Garbage collection: Java application servers' Achilles heel
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• Automated Testing and Debugging of SAT and QBF Solvers
• The Mechanical Verification of a DPLL-Based Satisfiability Solver
• Formal certification of a compiler back-end or
• Rocket-Fast Proof Checking for SMT Solvers
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Bounded model checking using satisfiability solving

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