Safety Property Verification Using Sequential SAT and Bounded Model Checking

Model checkers verify properties of safety- or business-critical systems. The main idea behind model checking is to convert a designʹs verification into a problem of checking key design properties expressed as a set of temporal logic formulas. The graph representing the designʹs state space then becomes the basis for testing these formulasʹ satisfiability (SAT). This divide-and-conquer approach provides an overall test for design correctness. We describe a method for checking safety properties using sequential SAT. SSAT can efficiently prove true properties by harnessing the power of bounded model checking (BMC) using SAT, but without the need for a pre-computed correctness threshold. Using a standard set of benchmarks, we conducted experiments to compare the runtime behavior of SSAT with BMC and binary decision diagrams (BDDs).