BMC Completeness Threshold

In bounded model checking (BMC), unrolling the transition relation up to depth k produces a formula $BMC_{k,k+d}(\psi, \phi)$ whose satisfiability witnesses a counterexample trace of length up to k + d. As k grows, more potential counterexamples are exposed, but unbounded verification is impossible without additional machinery.

Definition

The BMC completeness threshold CT is a depth such that, once a BMC instance of that depth (augmented with a no-self-loop predicate or an exit-state predicate) is found to be unsatisfiable, one can conclude that no counterexample trace of any length exists for the property at hand. In other words, CT bounds the number of steps after which completeness of verification can be declared.

Form used in HMC

Within hybrid model checking (HMC), the no-self-loop formulation used as a completeness criterion is

$$LFP_{k,k+d} \equiv BMC_{k,k+d}(\psi, \phi) \wedge \bigwedge_{k \le i < j \le k+d} (s_i \neq s_j)$$

When this formula is unsatisfiable, the threshold CT is considered reached, and verification is complete up to depth k + d for properties expressed over the state set ψ.

An improved variant that only checks whether the last state can reach a designated SINK (exit) control state reduces the resulting SAT formula to size O(d) rather than O(d²):

$$NTP_{k,k+d} \equiv BMC_{k,k+d}(\psi, \phi) \wedge (\phi = B_{SINK})$$

Because for terminating programs the SINK control state has no outgoing transitions, this predicate suffices for completeness in the terminating case.

Relation to HMC termination guarantees

HMC avoids accumulating the entire reachable state set, so it cannot generally detect a reachable fixpoint. However, by relying on the BMC completeness threshold (CT) for terminating programs and on frontier-set traversal bounded by the longest program path L, HMC can guarantee termination: state traversal terminates after L steps, and path-based reasoning declares completeness once the CT-based formula becomes unsatisfiable.

Role in reducing BMC instance size

Because the number of abstract control paths in an unrolled CFG grows rapidly with depth k, replacing some of the unrolled transitions by the set of concrete reachable states shrinks later BMC instances. The CT-based criterion tells HMC when it is safe to perform such replacement without losing completeness, allowing deeper BMC search in practice.