Interpolation and SAT-Based Model Checking

Abstract. We consider a fully SAT-based method of unbounded symbolic model checking based on computing Craig interpolants. In benchmark studies using a set of large industrial circuit verification instances, this method is greatly more efficient than BDD-based symbolic model checking, and compares favorably to some recent SAT-based model checking methods on positive instances.

• Type: Conference
• Year: 2003
• Where: CAV
• Authors: Kenneth L. McMillan
• Keywords: CAV 2003, Formal Methods, SAT-based Method, Symbolic Model Checking, Unbounded Symbolic Model