An automated SAT encoding-verification approach for efficient model checking
Khaza Anuarul Hoque, Otmane Aı̈t Mohamed, Sa’ed Abed, Mounir Boukadoum · 2010
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.