Unbounded Model Checking

SAT-based Bounded Model Checking (BMC) [45, 66, 109, 178] has been shown to be more robust and scalable compared to symbolic model checking methods based on Binary Decision Diagrams (BDDs) [12, 17]. Unlike BDD-based methods, BMC focuses on finding bugs of bounded length, successively increasing the bound to search for longer traces. Although BMC can find bugs in larger designs than BDD-based methods, the correctness of a property is guaranteed only for the analysis bound. A completeness bound has been proposed [66, 67, 72], to provide a proof of correctness for safety properties based on the longest loop-free path between states. Unfortunately, the longest loop-free path can be exponentially longer than the reachable diameter of the state space (for example the longest loopfree path for an n-bit counter is 2ⁿ while the reachable diameter is 1). One can use inductive invariants like reachability constraints [73] to obtain proofs earlier than the longest loop-free path. Alternatively, one can obtain a shorter completeness bound, i.e., the longest shortest backward diameter, for BMC using SAT-based fixed-point computations [67], described in the procedure Fixed_point_EF (see Figure 2.10). Such an approach uses cubewise enumeration of SAT solutions, as described in the procedure All_sat (see Figure 2.9), for computing exisitential quantifications.