Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/596
Title: | Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL | Authors: | Marić, Filip | Affiliations: | Informatics and Computer Science | Keywords: | DPLL procedure;Formal program verification;Isabelle;SAT problem | Issue Date: | 12-Nov-2010 | Journal: | Theoretical Computer Science | Abstract: | We present a formalization and a formal total correctness proof of a MiniSAT-like SAT solver within the system Isabelle/HOL. The solver is based on the DPLL procedure and employs most state-of-the-art SAT solving techniques, including the conflict-guided backjumping, clause learning, and the two-watched unit propagation scheme. A shallow embedding into Isabelle/HOL is used and the solver is expressed as a set of recursive HOL functions. Based on this specification, the Isabelle's built-in code generator can be used to generate executable code in several supported functional languages (Haskell, SML, and OCaml). The SAT solver implemented in this way is, to our knowledge, the first fully formally and mechanically verified modern SAT solver. © 2010 Elsevier B.V. All rights reserved. |
URI: | https://research.matf.bg.ac.rs/handle/123456789/596 | ISSN: | 03043975 | DOI: | 10.1016/j.tcs.2010.09.014 |
Appears in Collections: | Research outputs |
Show full item record
SCOPUSTM
Citations
49
checked on Dec 20, 2024
Page view(s)
10
checked on Dec 23, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.