6
D. Beyer and M. Dangl
make the step to y = z due to the inequalities between w and y, and x and z,
respectively.
• For consistency with our evaluation, we also applied a data-flow analysis
based on a template for tracking whether a variable is even or odd; obviously
this is not useful for this program, and thus, this configuration also fails.
• Even combining the previous three techniques into a compound invariant
generator that computes auxiliary invariants for k -induction does not yield a
successful configuration for this verification task.
• The invariant generator KIPDR (the above-mentioned adaptation of PDR to
k -induction, which we present in more detail in Sect. 3), however, detects the
invariant y = z and is therefore able to construct a proof by induction for
this verification task.
We will now briefly sketch how KIPDR detects the invariant y = z for the
example verification task. At first, KIPDR attempts to prove by induction that
when line 18 is reached, the assertion condition holds, which fails as discussed
previously. However, this failed induction attempt yields a counterexample to
induction where the values of y and z differ from each other, e.g., y = 0 ∧ z = 1,
which is then generalized to y
= z, i.e., a set of states that includes the concrete
predecessor of a bad state from the counterexample, as well as many other states
that would violate the assertion, if they were reachable themselves. Then, KIPDR
attempts to find an inductive invariant that eliminates all of these states, and
the attempt succeeds with the invariant y = z. Afterwards, KIPDR re-attempts
its original induction proof to show that the assertion is never violated, which
now succeeds due to the auxiliary invariant y = z.
Contributions. We present the following contributions:
• We implement one adaptation of PDR to software verification (based
on [11, 20]) in the open-source verification framework CPAchecker, in order
to establish a baseline for comparison with new ideas for improvement.
• We design and implement the algorithm KIPDR, as a new module for
invariant generation that is based on ideas from PDR and use this module
as an extension to a state-of-the-art approach to k -induction [5].
• We conduct a large experimental study to compare several tools and approaches to software verification using PDR as a component, to highlight
strengths and weaknesses of PDR in the domain of software verification.
• We contribute a set of small examples that need invariants that are more
difficult to obtain for standard data-flow-based approaches than the invariants
necessary for programs in the large benchmark set.
Related Work. While PDR (also known as IC3 for its first implementation [12])
was introduced as a SAT-based algorithm for model checking finite-state Boolean
transition systems [13], several approaches have since then been presented to
extend it to SMT and to apply it to the verification of software models: PDR
has been suggested as an interpolation engine for Impact, but experiments have
shown that it is too expensive in the general case, and is most effective if only
D. Beyer and M. Dangl
make the step to y = z due to the inequalities between w and y, and x and z,
respectively.
• For consistency with our evaluation, we also applied a data-flow analysis
based on a template for tracking whether a variable is even or odd; obviously
this is not useful for this program, and thus, this configuration also fails.
• Even combining the previous three techniques into a compound invariant
generator that computes auxiliary invariants for k -induction does not yield a
successful configuration for this verification task.
• The invariant generator KIPDR (the above-mentioned adaptation of PDR to
k -induction, which we present in more detail in Sect. 3), however, detects the
invariant y = z and is therefore able to construct a proof by induction for
this verification task.
We will now briefly sketch how KIPDR detects the invariant y = z for the
example verification task. At first, KIPDR attempts to prove by induction that
when line 18 is reached, the assertion condition holds, which fails as discussed
previously. However, this failed induction attempt yields a counterexample to
induction where the values of y and z differ from each other, e.g., y = 0 ∧ z = 1,
which is then generalized to y
= z, i.e., a set of states that includes the concrete
predecessor of a bad state from the counterexample, as well as many other states
that would violate the assertion, if they were reachable themselves. Then, KIPDR
attempts to find an inductive invariant that eliminates all of these states, and
the attempt succeeds with the invariant y = z. Afterwards, KIPDR re-attempts
its original induction proof to show that the assertion is never violated, which
now succeeds due to the auxiliary invariant y = z.
Contributions. We present the following contributions:
• We implement one adaptation of PDR to software verification (based
on [11, 20]) in the open-source verification framework CPAchecker, in order
to establish a baseline for comparison with new ideas for improvement.
• We design and implement the algorithm KIPDR, as a new module for
invariant generation that is based on ideas from PDR and use this module
as an extension to a state-of-the-art approach to k -induction [5].
• We conduct a large experimental study to compare several tools and approaches to software verification using PDR as a component, to highlight
strengths and weaknesses of PDR in the domain of software verification.
• We contribute a set of small examples that need invariants that are more
difficult to obtain for standard data-flow-based approaches than the invariants
necessary for programs in the large benchmark set.
Related Work. While PDR (also known as IC3 for its first implementation [12])
was introduced as a SAT-based algorithm for model checking finite-state Boolean
transition systems [13], several approaches have since then been presented to
extend it to SMT and to apply it to the verification of software models: PDR
has been suggested as an interpolation engine for Impact, but experiments have
shown that it is too expensive in the general case, and is most effective if only