Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/518
Title: Formalization of abstract state transition systems for SAT
Authors: Marić, Filip 
Janičić, Predrag 
Affiliations: Informatics and Computer Science 
Informatics and Computer Science 
Keywords: Abstract state transition systems;Formal verification;Isabelle/hol;Sat solving
Issue Date: 8-Nov-2011
Rank: M22
Publisher: EPI Sciences
Journal: Logical Methods in Computer Science
Abstract: 
We 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ć.
URI: https://research.matf.bg.ac.rs/handle/123456789/518
DOI: 10.2168/LMCS-7(3:19)2011
Rights: Attribution 3.0 United States
Appears in Collections:Research outputs

Files in This Item:
File Description SizeFormat
1108.4368.pdf421.96 kBAdobe PDF
View/Open
Show full 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