Questions: Bounded Model Checking

Question 1

Bounded model checking encodes the question 'does a property violation exist within k steps?' as a SAT formula. What are the main components of this encoding?

• A. Only the initial state and the property to be checked
• B. The initial state constraint I(s_0), the transition relation T(s_i, s_{i+1}) unrolled k times, and the negation of the property at each step (disjunction of bad states across steps 0 through k)
• C. A BDD representing all reachable states and a CTL formula
• D. The program source code translated directly to CNF

Answer: (B)

The BMC encoding creates Boolean variables for the state at each time step s_0, s_1, ..., s_k. The formula is: I(s_0) AND T(s_0,s_1) AND T(s_1,s_2) AND ... AND T(s_{k-1},s_k) AND (NOT P(s_0) OR NOT P(s_1) OR ... OR NOT P(s_k)), where I is the initial state predicate, T is the transition relation, and P is the safety property. A satisfying assignment gives concrete state values at each step -- a counterexample trace. If UNSAT, no violation exists in k steps. The formula size grows linearly with k, making deep unrolling feasible with modern SAT solvers.

Question 2

BDD-based symbolic model checking computes the exact set of reachable states, while bounded model checking does not. Why is BMC often more effective at finding bugs in practice?

Model answer: BDD-based model checking builds a BDD representing ALL reachable states, which can blow up exponentially in the number of state variables (the BDD size is highly sensitive to variable ordering and system structure). BMC avoids constructing the full reachable state set -- it only asks whether a counterexample of bounded length exists. Modern SAT solvers handle formulas with millions of variables through conflict-driven clause learning (CDCL), which exploits the structure of the specific instance. For bug finding, BMC is superior because bugs typically manifest as short counterexamples, and SAT solvers are remarkably efficient at finding satisfying assignments (or proving unsatisfiability) for structured industrial formulas.

The empirical dominance of SAT-based BMC over BDD-based methods for bug finding was demonstrated convincingly by Biere, Cimatti, Clarke, and Zhu (1999). Key insight: for verification (proving absence of bugs), BDD methods may still be necessary since BMC at depth k only proves safety up to k steps. However, k-induction and Craig interpolation extend BMC toward complete verification.

Question 3

K-induction strengthens bounded model checking to achieve complete verification (not just bounded bug-finding). The induction step checks whether any state satisfying the property for k consecutive steps must also satisfy it at step k+1.

• T. True
• F. False

Answer: True

K-induction has two parts: (1) the base case checks that the property holds for all states reachable in 0 to k steps from the initial states (standard BMC with UNSAT result), and (2) the induction step checks: for ANY sequence of k+1 states satisfying the transition relation, if the property holds at steps 0 through k-1, does it hold at step k? If the induction step is also UNSAT (no counterexample to the inductive hypothesis), the property holds for all reachable states at any depth. The parameter k controls the strength of the induction: k=1 is standard induction, larger k handles properties that require stronger inductive invariants. K-induction is complete for finite-state systems (some k suffices) but finding the right k may require auxiliary invariants.

Question 4

Craig interpolation is used in BMC-based verification to derive an overapproximation of the reachable states from an unsatisfiability proof. Why is this useful for proving unbounded safety properties?

Model answer: When a BMC formula at depth k is UNSAT, the SAT solver produces a proof of unsatisfiability. Craig's interpolation theorem guarantees that from a proof that A AND B is unsatisfiable, one can extract a formula (the interpolant) that is implied by A, inconsistent with B, and uses only variables common to A and B. In BMC, A encodes the first i transition steps and B encodes the remaining steps plus the property violation. The interpolant overapproximates the states reachable in i steps. Iteratively computing interpolants for increasing depths builds an overapproximation of the full reachable state set. If this overapproximation stabilizes (reaches a fixed point) and excludes all bad states, unbounded safety is proven -- without ever computing the exact reachable state set.

McMillan (2003) introduced interpolation-based model checking, which combines the bug-finding power of SAT-based BMC with the completeness of image computation. The key advantage over BDD-based approaches is that interpolants are computed from SAT proofs (leveraging CDCL efficiency) rather than BDD operations (which suffer from variable ordering sensitivity). This approach has been highly successful in hardware verification, where systems have enormous state spaces but structured transition relations.