DocumentCode
2256572
Title
An automated SAT encoding-verification approach for efficient model checking
Author
Hoque, Khaza Anuarul ; Mohamed, O. Ait ; Abed, Sa Ed ; Boukadoum, Mounir
fYear
2010
fDate
19-22 Dec. 2010
Firstpage
419
Lastpage
422
Abstract
In this paper, we introduce an automated conversion-verification methodology to convert a Directed Formula (DF) into a Conjunctive Normal Form (CNF) formula that can be fed to a SAT solver. In addition, the formal verification of this conversion is conducted within the HOL theorem prover. Finally, we conduct experimental results with different-sized formulas to show the effectiveness of our methodology.
Keywords
computability; formal verification; theorem proving; HOL theorem prover; SAT solver; automated SAT encoding-verification approach; automated conversion-verification methodology; conjunctive normal form formula; different-sized formulas; directed formula; efficient model checking; formal verification; Boolean functions; Converters; Data structures; Encoding; Engines; Generators; Logic gates;
fLanguage
English
Publisher
ieee
Conference_Titel
Microelectronics (ICM), 2010 International Conference on
Conference_Location
Cairo
Print_ISBN
978-1-61284-149-6
Type
conf
DOI
10.1109/ICM.2010.5696177
Filename
5696177
Link To Document