12
D. Beyer and M. Dangl
by the transition relation T , and the set of safe states is described by the
safety property P . The accessor get_currently_known_invariant is used to
obtain the strongest invariant currently available via a concurrently running
(external) auxiliary-invariant generator. A Boolean flag pd (reminding of
“property-directed”) is used to control whether or not failed induction checks
are used to guide the algorithm towards a sufficient strengthening of the safety
property P to prove correctness; if pd is set to false, the algorithm behaves
exactly like standard k -induction. Given a failed attempt to prove some candidate
invariant Q
5
by induction, the function lift is used to obtain from a concrete
counterexample-to-induction (CTI) state a set of CTI states described by a
state predicate C. An implementation of the function lift needs to satisfy the
condition that for a CTI s ∈ S where S is the set of program states, k ∈ N,
Inv ∈ (S → B), Q ∈ (S → B), and C = lift(k, Inv , Q, s), the following holds:
C(s) ∧
∀s n ∈ S : C(s n ) ⇒ Inv (s n ) ∧
n+k−1
i=n
(Q(s i ) ∧ T (s i ,s i+1 )) ⇒ ¬Q(s n+k )
,
which means that the CTI s must be an element of the set of states described by
the resulting predicate C and that all states in this set must be CTIs, i.e., they
need to be k-predecessors of ¬Q-states, or in other words, each state in the set of
states described by the predicate C must reach some ¬Q-state via k unrollings of
the transition relation T . We can implement lift using Craig interpolation [18, 30]
between A : s = s n and B : Inv (s n ) ∧
n+k−1
i=n
(Q(s i ) ∧ T (s i , s i+1 )) ⇒ ¬Q(s n+k ),
because s is a CTI, and therefore we know that A ⇒ B holds.
6
Hence, the resulting interpolant satisfies the criteria for C to be a valid lifting of s according to the
requirements towards the function lift as outlined above. The function strengthen
is used to obtain for a k-inductive invariant a stronger k-inductive invariant, i.e.,
its result needs to imply the input invariant, and, just like the input invariant, it
must not be violated within k loop iterations and must be k-inductive.
Algorithm. Lines 4 to 6 show the base-case check (BMC) and lines 7 to 9
show the forward-condition check, both as described in Sect. 2. If pd is set
to true, lines 10 to 23 attempt to prove each proof obligation using k -induction:
Lines 12 to 14 check the base case for a proof obligation o. If any violations
of the proof obligation o are found, this means that a predecessor state of
a ¬P -state, and thus, transitively, a ¬P -state, is reachable, so we return false. If,
otherwise, no violation was found, lines 16 to 23 check the inductive-step case
to prove o.
7
We strengthen the induction hypothesis of the step-case check by
5 Depending on the step the algorithm is in, Q may be either the safety property P or
a proof obligation o.
6 The formula C is called Craig interpolant for two formulas A and B with A ⇒ B, if
A ⇒ C, C ⇒ B, and all variables in C occur in both A and B.
7 Note that we do not need to check the forward condition for proof obligations, because
the forward condition is unrelated to the safety property and the proof obligations,
and therefore only needs to be checked once in each major iteration (i.e., once after
each increment of k).
D. Beyer and M. Dangl
by the transition relation T , and the set of safe states is described by the
safety property P . The accessor get_currently_known_invariant is used to
obtain the strongest invariant currently available via a concurrently running
(external) auxiliary-invariant generator. A Boolean flag pd (reminding of
“property-directed”) is used to control whether or not failed induction checks
are used to guide the algorithm towards a sufficient strengthening of the safety
property P to prove correctness; if pd is set to false, the algorithm behaves
exactly like standard k -induction. Given a failed attempt to prove some candidate
invariant Q
5
by induction, the function lift is used to obtain from a concrete
counterexample-to-induction (CTI) state a set of CTI states described by a
state predicate C. An implementation of the function lift needs to satisfy the
condition that for a CTI s ∈ S where S is the set of program states, k ∈ N,
Inv ∈ (S → B), Q ∈ (S → B), and C = lift(k, Inv , Q, s), the following holds:
C(s) ∧
∀s n ∈ S : C(s n ) ⇒ Inv (s n ) ∧
n+k−1
i=n
(Q(s i ) ∧ T (s i ,s i+1 )) ⇒ ¬Q(s n+k )
,
which means that the CTI s must be an element of the set of states described by
the resulting predicate C and that all states in this set must be CTIs, i.e., they
need to be k-predecessors of ¬Q-states, or in other words, each state in the set of
states described by the predicate C must reach some ¬Q-state via k unrollings of
the transition relation T . We can implement lift using Craig interpolation [18, 30]
between A : s = s n and B : Inv (s n ) ∧
n+k−1
i=n
(Q(s i ) ∧ T (s i , s i+1 )) ⇒ ¬Q(s n+k ),
because s is a CTI, and therefore we know that A ⇒ B holds.
6
Hence, the resulting interpolant satisfies the criteria for C to be a valid lifting of s according to the
requirements towards the function lift as outlined above. The function strengthen
is used to obtain for a k-inductive invariant a stronger k-inductive invariant, i.e.,
its result needs to imply the input invariant, and, just like the input invariant, it
must not be violated within k loop iterations and must be k-inductive.
Algorithm. Lines 4 to 6 show the base-case check (BMC) and lines 7 to 9
show the forward-condition check, both as described in Sect. 2. If pd is set
to true, lines 10 to 23 attempt to prove each proof obligation using k -induction:
Lines 12 to 14 check the base case for a proof obligation o. If any violations
of the proof obligation o are found, this means that a predecessor state of
a ¬P -state, and thus, transitively, a ¬P -state, is reachable, so we return false. If,
otherwise, no violation was found, lines 16 to 23 check the inductive-step case
to prove o.
7
We strengthen the induction hypothesis of the step-case check by
5 Depending on the step the algorithm is in, Q may be either the safety property P or
a proof obligation o.
6 The formula C is called Craig interpolant for two formulas A and B with A ⇒ B, if
A ⇒ C, C ⇒ B, and all variables in C occur in both A and B.
7 Note that we do not need to check the forward condition for proof obligations, because
the forward condition is unrelated to the safety property and the proof obligations,
and therefore only needs to be checked once in each major iteration (i.e., once after
each increment of k).