versat: A Verified Modern SAT Solver
From MaRDI portal
Publication:2891429
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
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
