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

DOI10.1016/j.tcs.2010.09.014zbMath1208.68205MaRDI 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 problem; Isabelle; DPLL procedure; formal program verification

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Related Items

SAT Solver Verification

Uses Software

• Isabelle
• MiniSat
• Isabelle/HOL
• SATO
• OCaml
• Chaff
• BerkMin
• Archive Formal Proofs