Title :
An automated SAT encoding-verification approach for efficient model checking
Author :
Hoque, Khaza Anuarul ; Mohamed, O. Ait ; Abed, Sa Ed ; Boukadoum, Mounir
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;
Conference_Titel :
Microelectronics (ICM), 2010 International Conference on
Conference_Location :
Cairo
Print_ISBN :
978-1-61284-149-6
DOI :
10.1109/ICM.2010.5696177
