1. Research with MATF
  2. MATF
  3. Research outputs
Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/596
DC FieldValueLanguage
dc.contributor.authorMarić, Filipen_US
dc.date.accessioned2022-08-13T15:50:04Z-
dc.date.available2022-08-13T15:50:04Z-
dc.date.issued2010-11-12-
dc.identifier.issn03043975en
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/596-
dc.description.abstractWe 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.en
dc.relation.ispartofTheoretical Computer Scienceen_US
dc.subjectDPLL procedureen
dc.subjectFormal program verificationen
dc.subjectIsabelleen
dc.subjectSAT problemen
dc.titleFormal verification of a modern SAT solver by shallow embedding into Isabelle/HOLen_US
dc.typeArticleen_US
dc.identifier.doi10.1016/j.tcs.2010.09.014-
dc.identifier.scopus2-s2.0-78049318372-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/78049318372-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.firstpage4333en_US
dc.relation.lastpage4356en_US
dc.relation.volume411en_US
dc.relation.issue50en_US
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.openairetypeArticle-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0001-7219-6960-
Appears in Collections:Research outputs
Show simple item record

SCOPUSTM   
Citations

49
checked on Dec 20, 2024

Page view(s)

10
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.