Software Verification with PDR: An Implementation of the State of the Art
9
F i
c 1 c 2
c 3
c 4
c 5
T
⇒ c 4
F i+1
∧ c 4
T
⇒
(a) Consecution check makes sure
to only conjoin to frame Fi+1
such ci from Fi that are inductive relative to Fi w.r.t. transition
relation T
F k
P
t
⇓
t, k − 1
F k−1
F k
P
t
¬c
c
F k−1
F k
P
u
t
⇓
u, k − 2
or
(b) If phase 1 results in a proof obligation t, k − 1
(top), then phase 2 resolves either by strengthening
F k with c (left), or by creating a new (backwards)
proof obligation u, k−2 (right); if the chain of proof
obligations propagates back to the initial states, then
a feasible error path is found
Fig. 2: Visualization of (a) the consecution check and (b) the handling of proofobligations.
2.2 k -Induction
Like PDR, k -induction attempts to prove a safety property P by applying
induction. However, while PDR strengthens its induction hypothesis by using
clauses extracted from specific counterexamples to induction after failed induction
attempts, k -induction strengthens its induction hypothesis by increasing the
length of the unrolling of the transition relation.
Starting with an initial value for the bound k (usually 1), the k -induction
algorithm increases the value of k iteratively after each unsuccessful attempt at
finding a specification violation (base case), proving correctness via complete
loop unrolling (forward condition), or inductively proving correctness of the
program (inductive-step case).
Base Case. The base case of k -induction consists of running BMC with the
current bound k.
4
This means that starting from all initial program states, all
4 We define the loop bound as the number of visits of the loop head, that is, with loop
bound k = 1, the loop head is visited once, but there was not yet any unwinding
of the loop body. This nicely matches the intuition for k-induction: 1-inductiveness
means that if the invariant holds for one state (without loop unrolling), then it holds
again after one loop unrolling in the successor state; k-inductiveness means that if
the invariant holds for k states (k − 1 loop unrollings), then it holds again after one
more loop unrolling in the successor state.
9
F i
c 1 c 2
c 3
c 4
c 5
T
⇒ c 4
F i+1
∧ c 4
T
⇒
(a) Consecution check makes sure
to only conjoin to frame Fi+1
such ci from Fi that are inductive relative to Fi w.r.t. transition
relation T
F k
P
t
⇓
t, k − 1
F k−1
F k
P
t
¬c
c
F k−1
F k
P
u
t
⇓
u, k − 2
or
(b) If phase 1 results in a proof obligation t, k − 1
(top), then phase 2 resolves either by strengthening
F k with c (left), or by creating a new (backwards)
proof obligation u, k−2 (right); if the chain of proof
obligations propagates back to the initial states, then
a feasible error path is found
Fig. 2: Visualization of (a) the consecution check and (b) the handling of proofobligations.
2.2 k -Induction
Like PDR, k -induction attempts to prove a safety property P by applying
induction. However, while PDR strengthens its induction hypothesis by using
clauses extracted from specific counterexamples to induction after failed induction
attempts, k -induction strengthens its induction hypothesis by increasing the
length of the unrolling of the transition relation.
Starting with an initial value for the bound k (usually 1), the k -induction
algorithm increases the value of k iteratively after each unsuccessful attempt at
finding a specification violation (base case), proving correctness via complete
loop unrolling (forward condition), or inductively proving correctness of the
program (inductive-step case).
Base Case. The base case of k -induction consists of running BMC with the
current bound k.
4
This means that starting from all initial program states, all
4 We define the loop bound as the number of visits of the loop head, that is, with loop
bound k = 1, the loop head is visited once, but there was not yet any unwinding
of the loop body. This nicely matches the intuition for k-induction: 1-inductiveness
means that if the invariant holds for one state (without loop unrolling), then it holds
again after one loop unrolling in the successor state; k-inductiveness means that if
the invariant holds for k states (k − 1 loop unrollings), then it holds again after one
more loop unrolling in the successor state.