4
D. Beyer and M. Dangl
While in theory, given the aforementioned body of work on the topic, the
advantages and disadvantages of using PDR seem clear, we are interested in
understanding the effect of applying PDR to a large set of verification tasks
that were collected from academia and also from industrial software, such as
the Linux kernel. To achieve this goal, we implemented one PDR adaptation for
software verification, and another approach that integrates a PDR-like invariantgeneration module into a k -induction approach.
PDR Adaptation for Software Verification. PDR is a model-checking algorithm
that tries to construct an inductive safety invariant by incrementally learning
clauses that are inductive relative to previously learned clauses. The clauselearning strategy is guided by counterexamples to induction, i.e., each time a
proof of inductiveness fails, the algorithm attempts to learn a new clause to avoid
the same counterexample to induction in the future. Originally, this algorithm
was designed as a SAT-based technique for Boolean finite-state systems. Every
adaptation of PDR to software verification therefore needs to consider how to
effectively and efficiently handle the infinite state space and how to transfer
the algorithm from SAT to SMT. Furthermore, the adaptation to software has
to deal with the program counter.
PDR-like Invariant Generation. Whenever an induction-proof attempt fails with
a counterexample, the counterexample describes a state s that can transition
into a bad state (that violates the safety property), which means that in order to
make the proof succeed, s must be removed from consideration by an auxiliary
invariant. From this bad-state predecessor s, the clause-learning strategy of
PDR proceeds to generate such an auxiliary invariant by applying the following
two steps: (1) s is first generalized to a set of states C that all transition into
a bad state; (2) an invariant is constructed that is (a) inductive relative to
previously found invariants
1
and (b) at least strong enough to eliminate all
states in C. If it fails to construct such an invariant and prove its inductiveness,
then the steps are recursively re-applied to the counterexample obtained from
the failed induction attempt.
We experimentally investigate two implementations of adaptations of PDR
to software verification (CPAchecker-CTIGAR and Vvt-CTIGAR), as well as
several combinations that use the PDR-like invariant-generation module that
we designed and implemented for this study.
Example. Figure 1 shows an example C program (eq2.c) that contains four
unsigned integer variables w, x, y, and z. In line 10, the variable w is initialized to
an unknown value via the input function __VERIFIER_nondet_uint(); then, its
value is copied to x in line 11. In line 12, variable y is initialized with the value
of w + 1, and in line 13, variable z is initialized with the value of x + 1, such
1 An assertion F is said to be inductive relative to an invariant Inv if
Inv can be used as an auxiliary invariant for the proof of inductiveness ∀sj, sj+1 : F (sj) ∧ T (sj, sj+1) ⇒ F (sj+1) by conjoining Inv to the
induction hypothesis F (sj), such that the modified induction query
∀sj, sj+1 : F (sj) ∧ Inv (s j ) ∧ T (sj, sj+1) ⇒ F (sj+1) allows a proof by induction to
succeed. [12]
D. Beyer and M. Dangl
While in theory, given the aforementioned body of work on the topic, the
advantages and disadvantages of using PDR seem clear, we are interested in
understanding the effect of applying PDR to a large set of verification tasks
that were collected from academia and also from industrial software, such as
the Linux kernel. To achieve this goal, we implemented one PDR adaptation for
software verification, and another approach that integrates a PDR-like invariantgeneration module into a k -induction approach.
PDR Adaptation for Software Verification. PDR is a model-checking algorithm
that tries to construct an inductive safety invariant by incrementally learning
clauses that are inductive relative to previously learned clauses. The clauselearning strategy is guided by counterexamples to induction, i.e., each time a
proof of inductiveness fails, the algorithm attempts to learn a new clause to avoid
the same counterexample to induction in the future. Originally, this algorithm
was designed as a SAT-based technique for Boolean finite-state systems. Every
adaptation of PDR to software verification therefore needs to consider how to
effectively and efficiently handle the infinite state space and how to transfer
the algorithm from SAT to SMT. Furthermore, the adaptation to software has
to deal with the program counter.
PDR-like Invariant Generation. Whenever an induction-proof attempt fails with
a counterexample, the counterexample describes a state s that can transition
into a bad state (that violates the safety property), which means that in order to
make the proof succeed, s must be removed from consideration by an auxiliary
invariant. From this bad-state predecessor s, the clause-learning strategy of
PDR proceeds to generate such an auxiliary invariant by applying the following
two steps: (1) s is first generalized to a set of states C that all transition into
a bad state; (2) an invariant is constructed that is (a) inductive relative to
previously found invariants
1
and (b) at least strong enough to eliminate all
states in C. If it fails to construct such an invariant and prove its inductiveness,
then the steps are recursively re-applied to the counterexample obtained from
the failed induction attempt.
We experimentally investigate two implementations of adaptations of PDR
to software verification (CPAchecker-CTIGAR and Vvt-CTIGAR), as well as
several combinations that use the PDR-like invariant-generation module that
we designed and implemented for this study.
Example. Figure 1 shows an example C program (eq2.c) that contains four
unsigned integer variables w, x, y, and z. In line 10, the variable w is initialized to
an unknown value via the input function __VERIFIER_nondet_uint(); then, its
value is copied to x in line 11. In line 12, variable y is initialized with the value
of w + 1, and in line 13, variable z is initialized with the value of x + 1, such
1 An assertion F is said to be inductive relative to an invariant Inv if
Inv can be used as an auxiliary invariant for the proof of inductiveness ∀sj, sj+1 : F (sj) ∧ T (sj, sj+1) ⇒ F (sj+1) by conjoining Inv to the
induction hypothesis F (sj), such that the modified induction query
∀sj, sj+1 : F (sj) ∧ Inv (s j ) ∧ T (sj, sj+1) ⇒ F (sj+1) allows a proof by induction to
succeed. [12]