Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/518
DC FieldValueLanguage
dc.contributor.authorMarić, Filipen_US
dc.contributor.authorJaničić, Predragen_US
dc.date.accessioned2022-08-13T10:14:43Z-
dc.date.available2022-08-13T10:14:43Z-
dc.date.issued2011-11-08-
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/518-
dc.description.abstractWe present a formalization of modern SAT solvers and their properties in a form of abstract state transition systems. SAT solving procedures are described as transition relations over states that represent the values of the solver's global variables. Several different SAT solvers are formalized, including both the classical DPLL procedure and its state-of-the-art successors. The formalization is made within the Isabelle/HOL system and the total correctness (soundness, termination, completeness) is shown for each presented system (with respect to a simple notion of satisfiability that can be manually checked). The systems are defined in a general way and cover procedures used in a wide range of modern SAT solvers. Our formalization builds up on the previous work on state transition systems for SAT, but it gives machine-verifiable proofs, somewhat more general specifications, and weaker assumptions that ensure the key correctness properties. The presented proofs of formal correctness of the transition systems can be used as a key building block in proving correctness of SAT solvers by using other verification approaches. © F. Marić and P. Janičić.en_US
dc.language.isoenen_US
dc.publisherEPI Sciencesen_US
dc.relation.ispartofLogical Methods in Computer Scienceen_US
dc.rightsAttribution 3.0 United States*
dc.rights.urihttp://creativecommons.org/licenses/by/3.0/us/*
dc.subjectAbstract state transition systemsen_US
dc.subjectFormal verificationen_US
dc.subjectIsabelle/holen_US
dc.subjectSat solvingen_US
dc.titleFormalization of abstract state transition systems for SATen_US
dc.typeArticleen_US
dc.identifier.doi10.2168/LMCS-7(3:19)2011-
dc.identifier.scopus2-s2.0-80355129508-
dc.identifier.isi000301228300019-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/80355129508-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.issn1860-5974en_US
dc.description.rankM22en_US
dc.relation.firstpageArticle no. 19en_US
dc.relation.volume7en_US
dc.relation.issue3en_US
item.fulltextWith Fulltext-
item.languageiso639-1en-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextopen-
item.openairetypeArticle-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0001-7219-6960-
crisitem.author.orcid0000-0001-8922-4948-
Appears in Collections:Research outputs
Files in This Item:
File Description SizeFormat
1108.4368.pdf421.96 kBAdobe PDF
View/Open
Show simple item record

SCOPUSTM   
Citations

10
checked on Dec 20, 2024

Page view(s)

13
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


This item is licensed under a Creative Commons License Creative Commons