Software Verification with PDR: An Implementation of the State of the Art
11
Algorithm 1 Iterative-Deepening k -Induction with Property Direction
Input: the initial value kinit ≥ 1 for the bound k,
an upper limit kmax for the bound k,
a function inc : N → N with ∀n ∈ N : inc(n) > n,
the initial states defined by the predicate I,
the transfer relation defined by the predicate T ,
a safety property P ,
a function get_currently_known_invariant to obtain auxiliary invariants,
a Boolean pd that enables or disables property direction,
a function lift : N × (S → B) × (S → B) × S → (S → B), and
a function strengthen : N × (S → B) × (S → B) → (S → B),
where S is the set of program states.
Output: true if P holds, false otherwise
Variables: the current bound k := kinit,
the invariant InternalInv := true computed by this algorithm internally, and
the set O := {} of current proof obligations.
1: while k ≤ kmax do
2:
Oprev := O
3:
O := {}
4:
base_case := I(s0) ∧
k−1
n=0
n−1
i=0
T (si, si+1) ∧ ¬P (sn)
5:
if sat(base_case) then
6:
return false
7:
forward _condition := I(s0) ∧
k−1
i=0
T (si, si+1)
8:
if ¬ sat(forward _condition) then
9:
return true
10:
if pd then
11:
for each o ∈ Oprev do
12:
base_case o := I(s0) ∧
k−1
n=0
n−1
i=0
T (si, si+1) ∧ ¬o(sn)
13:
if sat(base_caseo) then
14:
return false
15:
else
16:
step_caseo n :=
n+k−1
i=n
(o(si) ∧ T (si, si+1)) ∧ ¬o(sn+k)
17:
ExternalInv := get_currently_known_invariant()
18:
Inv := InternalInv ∧ ExternalInv
19:
if sat(Inv (sn) ∧ step_caseo n ) then
20:
so := satisfying predecessor state
21:
O := O ∪ {¬lift(k, Inv , o, so)}
22:
else
23:
InternalInv := InternalInv ∧ strengthen(k, Inv , o)
24:
step_case n :=
n+k−1
i=n
(P (si) ∧ T (si, si+1)) ∧ ¬P (sn+k)
25:
ExternalInv := get_currently_known_invariant()
26:
Inv := InternalInv ∧ ExternalInv
27:
if sat(Inv (sn) ∧ step_case n ) then
28:
if pd then
29:
s := satisfying predecessor state
30:
O := O ∪ {¬lift(k, Inv , P, s)}
31:
else
32:
return true
33:
k := inc(k)
34: return unknown