8
D. Beyer and M. Dangl
relevant to prove the correctness of a safety property P . For a given state s, the
notation F i (s) means that the predicate F i holds for state s. The index i of a
frame F i is called its level, and the frame F k is called the frontier, because it
represents the largest overapproximation of reachable states computed by the
algorithm [12]. The algorithm maintains the following invariants:
1. F 0 (s) = I(s), i.e., the first frame represents precisely the initial states.
2. ∀i ∈ {0, . . . , k} : F i (s) ⇒ P (s), i.e., every frame contains only states that
satisfy the safety property.
3. ∀i ∈ {0, . . . , k − 1} : F i (s) ⇒ F i+1 (s), i.e., a frame F i+1 represents in addition
such states that are reachable with i + 1 steps.
4. ∀i ∈ {0, . . . , k − 1} : F i (s) ∧ T (s, s
) ⇒ F i+1 (s
), i.e., each frame is inductive
relative to its predecessor.
Using these data structures and algorithm invariants, the algorithm attempts to
find either a counterexample to P or a 1-inductive invariant F i such that F i (s) ⇔
F i+1 (s) for some level i ∈ {0, . . . , k − 1}. Until either of these potential outcomes
is reached, PDR shifts back and forth between the following two phases:
1. If the set of states represented by the frontier F k does not contain any predecessor states of ¬P -states (i.e., ∀s j , s j+1 : F k (s j ) ∧ T (s j , s j+1 ) ⇒ P (s j+1 ),
called frontier-incrementation check), a new frontier F k+1 is created and
initialized to P . Subsequently, the algorithm attempts to push forward
3
each
predicate c of each frame F i with 0 ≤ i ≤ k for which the consecution check
F i (s j ) ∧ T (s j , s j+1 ) ⇒ c(s j+1 ) holds (see Fig. 2a). If, on the other hand, the
frontier-incrementation check fails, PDR extracts a ¬P -predecessor t in F k ,
which represents a counterexample to induction (CTI), from the failed query
as proof obligation t, k − 1 (see Fig. 2b, top).
2. While the queue of proof obligations is not empty, PDR processes the queue
by trying to prove for each proof obligation t, i that the CTI-state t is itself
not reachable from F i and therefore does not need to be considered as a
relevant ¬P -predecessor. For this proof, PDR chooses some predicate c ⇒ ¬t
with ∀s : F i (s) ⇒ c(s). PDR then checks if c is inductive relative to F i by
performing the consecution check F i (s j ) ∧ c(s j ) ∧ T (s j , s j+1 ) ⇒ c(s j+1 ). If
the consecution check succeeds, the frames F 1 , . . . , F i+1 can be strengthened
by adding c, thus ruling out the CTI t in these frames for the future (see
Fig. 2b, left). Also, unless i = k, we add a new proof obligation t, i + 1 to
the queue as an optimization to initiate forward propagation, because we
expect that the CTI-state s would otherwise be rediscovered later at a higher
level [11]. Otherwise, i.e., the consecution check does not succeed for clause c,
the algorithm extracts a predecessor u of t from the failed consecution check,
which is added as a new proof obligation u, i − 1 if i > 0 and t ∧ I is
unsatisfiable (see Fig. 2b, right). Otherwise, u represents the initial state of
a real counterexample to P .
An example of this algorithm is presented in a technical report [8, pp. 7–8]. A
more detailed presentation of PDR can be found in the literature [12].
3 By “push forward”, we mean to add a predicate c from frame Fi to frame Fi+1 [12].
D. Beyer and M. Dangl
relevant to prove the correctness of a safety property P . For a given state s, the
notation F i (s) means that the predicate F i holds for state s. The index i of a
frame F i is called its level, and the frame F k is called the frontier, because it
represents the largest overapproximation of reachable states computed by the
algorithm [12]. The algorithm maintains the following invariants:
1. F 0 (s) = I(s), i.e., the first frame represents precisely the initial states.
2. ∀i ∈ {0, . . . , k} : F i (s) ⇒ P (s), i.e., every frame contains only states that
satisfy the safety property.
3. ∀i ∈ {0, . . . , k − 1} : F i (s) ⇒ F i+1 (s), i.e., a frame F i+1 represents in addition
such states that are reachable with i + 1 steps.
4. ∀i ∈ {0, . . . , k − 1} : F i (s) ∧ T (s, s
) ⇒ F i+1 (s
), i.e., each frame is inductive
relative to its predecessor.
Using these data structures and algorithm invariants, the algorithm attempts to
find either a counterexample to P or a 1-inductive invariant F i such that F i (s) ⇔
F i+1 (s) for some level i ∈ {0, . . . , k − 1}. Until either of these potential outcomes
is reached, PDR shifts back and forth between the following two phases:
1. If the set of states represented by the frontier F k does not contain any predecessor states of ¬P -states (i.e., ∀s j , s j+1 : F k (s j ) ∧ T (s j , s j+1 ) ⇒ P (s j+1 ),
called frontier-incrementation check), a new frontier F k+1 is created and
initialized to P . Subsequently, the algorithm attempts to push forward
3
each
predicate c of each frame F i with 0 ≤ i ≤ k for which the consecution check
F i (s j ) ∧ T (s j , s j+1 ) ⇒ c(s j+1 ) holds (see Fig. 2a). If, on the other hand, the
frontier-incrementation check fails, PDR extracts a ¬P -predecessor t in F k ,
which represents a counterexample to induction (CTI), from the failed query
as proof obligation t, k − 1 (see Fig. 2b, top).
2. While the queue of proof obligations is not empty, PDR processes the queue
by trying to prove for each proof obligation t, i that the CTI-state t is itself
not reachable from F i and therefore does not need to be considered as a
relevant ¬P -predecessor. For this proof, PDR chooses some predicate c ⇒ ¬t
with ∀s : F i (s) ⇒ c(s). PDR then checks if c is inductive relative to F i by
performing the consecution check F i (s j ) ∧ c(s j ) ∧ T (s j , s j+1 ) ⇒ c(s j+1 ). If
the consecution check succeeds, the frames F 1 , . . . , F i+1 can be strengthened
by adding c, thus ruling out the CTI t in these frames for the future (see
Fig. 2b, left). Also, unless i = k, we add a new proof obligation t, i + 1 to
the queue as an optimization to initiate forward propagation, because we
expect that the CTI-state s would otherwise be rediscovered later at a higher
level [11]. Otherwise, i.e., the consecution check does not succeed for clause c,
the algorithm extracts a predecessor u of t from the failed consecution check,
which is added as a new proof obligation u, i − 1 if i > 0 and t ∧ I is
unsatisfiable (see Fig. 2b, right). Otherwise, u represents the initial state of
a real counterexample to P .
An example of this algorithm is presented in a technical report [8, pp. 7–8]. A
more detailed presentation of PDR can be found in the literature [12].
3 By “push forward”, we mean to add a predicate c from frame Fi to frame Fi+1 [12].