10
D. Beyer and M. Dangl
states of the program reachable within at most k − 1 unwindings of the transition
relation are explored. If a ¬P -state is found, the algorithm terminates.
Forward Condition. If no ¬P -state is found by the BMC in the base case, the
algorithm continues by performing the forward-condition check, which attempts
to prove that BMC fully explored the state space of the program by checking
that no state with distance k
> k − 1 to the initial state is reachable. If this
check is successful, the algorithm terminates.
Inductive-Step Case. The forward-condition check, however, can only prove
safety for programs with finite (and, in practice, short) loops. To prove safety
beyond the bound k, the algorithm applies induction: The inductive-step case
attempts to prove that after every sequence of k unrollings of the transition
relation that did not reach a ¬P -state, there can also be no subsequent transition
into a ¬P -state by unwinding the transition relation once more. In the realm
of model checking of software, however, the safety property P is often not
directly k-inductive for any value of k, thus causing the inductive-step-case check
to fail. It is therefore state-of-the-art practice to add auxiliary invariants to
this check to further strengthen the induction hypothesis and make it more
likely to succeed. Thus, the inductive-step case proves a program safe if the
following condition is unsatisfiable:
Inv (s n ) ∧
n+k−1
i=n
(P (s i ) ∧ T (s i , s i+1 )) ∧ ¬P (s n+k )
where Inv is an auxiliary invariant, and s n , . . . , s n+k is any sequence of states. If
this check fails, the induction attempt is inconclusive, and the program is neither
proved safe nor unsafe yet with the current value of k and the given auxiliary
invariant. In this case, the algorithm increases the value of k and starts over.
A detailed presentation of k -induction can be found in the literature [5, 6].
3 Combining k -Induction with PDR
Algorithm 1 shows an extension of k -induction with continuously-refined
invariants [5] that applies PDR’s aspect of learning from counterexamples to
induction and that can be applied both as a main proof engine as well as an invariant generator. This allows us to apply this extension of k -induction as an invariant
generator to a main k -induction procedure, similar to the KI
←−KI approach [5].
Inputs. The algorithm takes the following inputs: The value k init is used to
initialize the unrolling bound k, whereas the function inc is used to increase k
in line 33 after each major iteration of the algorithm, up to an upper limit
of k defined by the value k max enforced in line 3. The set of initial program
states is described by the predicate I, the possible state transitions are described
D. Beyer and M. Dangl
states of the program reachable within at most k − 1 unwindings of the transition
relation are explored. If a ¬P -state is found, the algorithm terminates.
Forward Condition. If no ¬P -state is found by the BMC in the base case, the
algorithm continues by performing the forward-condition check, which attempts
to prove that BMC fully explored the state space of the program by checking
that no state with distance k
> k − 1 to the initial state is reachable. If this
check is successful, the algorithm terminates.
Inductive-Step Case. The forward-condition check, however, can only prove
safety for programs with finite (and, in practice, short) loops. To prove safety
beyond the bound k, the algorithm applies induction: The inductive-step case
attempts to prove that after every sequence of k unrollings of the transition
relation that did not reach a ¬P -state, there can also be no subsequent transition
into a ¬P -state by unwinding the transition relation once more. In the realm
of model checking of software, however, the safety property P is often not
directly k-inductive for any value of k, thus causing the inductive-step-case check
to fail. It is therefore state-of-the-art practice to add auxiliary invariants to
this check to further strengthen the induction hypothesis and make it more
likely to succeed. Thus, the inductive-step case proves a program safe if the
following condition is unsatisfiable:
Inv (s n ) ∧
n+k−1
i=n
(P (s i ) ∧ T (s i , s i+1 )) ∧ ¬P (s n+k )
where Inv is an auxiliary invariant, and s n , . . . , s n+k is any sequence of states. If
this check fails, the induction attempt is inconclusive, and the program is neither
proved safe nor unsafe yet with the current value of k and the given auxiliary
invariant. In this case, the algorithm increases the value of k and starts over.
A detailed presentation of k -induction can be found in the literature [5, 6].
3 Combining k -Induction with PDR
Algorithm 1 shows an extension of k -induction with continuously-refined
invariants [5] that applies PDR’s aspect of learning from counterexamples to
induction and that can be applied both as a main proof engine as well as an invariant generator. This allows us to apply this extension of k -induction as an invariant
generator to a main k -induction procedure, similar to the KI
←−KI approach [5].
Inputs. The algorithm takes the following inputs: The value k init is used to
initialize the unrolling bound k, whereas the function inc is used to increase k
in line 33 after each major iteration of the algorithm, up to an upper limit
of k defined by the value k max enforced in line 3. The set of initial program
states is described by the predicate I, the possible state transitions are described