Software Verification with PDR: An Implementation of the State of the Art
13
conjoining auxiliary invariants from an external invariant generator (via a call to
get_currently_known_invariant) and the auxiliary invariant computed internally
from proof obligations that we successfully proved previously. If the step-case
check for o is unsuccessful, we extract the resulting CTI state, lift it to a set of
CTI states, and construct a new proof obligation so that we can later attempt to
prove that these CTI states are unreachable. If, on the other hand, the step-case
check for o is successful, we no longer track o in the set O of unproven proof
obligations (this case corresponds to line 22). We could now directly use the
proof obligation as an invariant, but instead, in line 23 we first try to strengthen
it into a stronger invariant that removes even more unreachable states from
future consideration before conjoining it to our internally computed auxiliary
invariant. In our implementation, we implement strengthen by attempting to
drop components from a (disjunctive) invariant and checking if the remaining
clause is still inductive. In lines 24 to 32, we check the inductive-step case for
the safety property P . This check is mostly analogous to the inductive-step
case check for the proof obligations described above, except that if the check
is successful, we immediately return true.
Note that Alg. 1 eagerly increases k, even if the set O of proof obligations is not
empty. This heuristic prevents the PDR part from iterating through long chains
of proof obligations, it rather delegates the unrolling to the k-induction part.
An in-depth discussion of a practical example of Alg. 1 is presented in a
technical report [8, pp. 12–14].
4 Evaluation
In this section, we present an extensive experimental study on the effectiveness
and efficiency of adaptations of PDR to software verification.
4.1 Compared Approaches
We use the following abbreviations to distinguish between the different techniques that we evaluated:
CTIGAR: CTIGAR [11] is an adaptation of PDR to software verification.
Our evaluation compares two implementations of CTIGAR, namely VvtCTIGAR from the tool Vvt and our own implementation CPAcheckerCTIGAR. Vvt [20] also provides a configuration that runs a parallel portfolio
combination of Vvt-CTIGAR and bounded model checking, which we call
Vvt-Portfolio.
KI: KI [5] denotes the plain k -induction algorithm without property direction
and without auxiliary invariants, i.e., we configure Alg. 1 such that pd = false
and get_currently_known_invariant() always returns true.
KIPDR: KIPDR denotes a configuration of Alg. 1 such that pd = true
and get_currently_known_invariant() always returns true, i.e., k -induction
with property direction but without additional auxiliary-invariant generation.
KIPDR is, like CTIGAR, an adaptation of PDR to software verification.
13
conjoining auxiliary invariants from an external invariant generator (via a call to
get_currently_known_invariant) and the auxiliary invariant computed internally
from proof obligations that we successfully proved previously. If the step-case
check for o is unsuccessful, we extract the resulting CTI state, lift it to a set of
CTI states, and construct a new proof obligation so that we can later attempt to
prove that these CTI states are unreachable. If, on the other hand, the step-case
check for o is successful, we no longer track o in the set O of unproven proof
obligations (this case corresponds to line 22). We could now directly use the
proof obligation as an invariant, but instead, in line 23 we first try to strengthen
it into a stronger invariant that removes even more unreachable states from
future consideration before conjoining it to our internally computed auxiliary
invariant. In our implementation, we implement strengthen by attempting to
drop components from a (disjunctive) invariant and checking if the remaining
clause is still inductive. In lines 24 to 32, we check the inductive-step case for
the safety property P . This check is mostly analogous to the inductive-step
case check for the proof obligations described above, except that if the check
is successful, we immediately return true.
Note that Alg. 1 eagerly increases k, even if the set O of proof obligations is not
empty. This heuristic prevents the PDR part from iterating through long chains
of proof obligations, it rather delegates the unrolling to the k-induction part.
An in-depth discussion of a practical example of Alg. 1 is presented in a
technical report [8, pp. 12–14].
4 Evaluation
In this section, we present an extensive experimental study on the effectiveness
and efficiency of adaptations of PDR to software verification.
4.1 Compared Approaches
We use the following abbreviations to distinguish between the different techniques that we evaluated:
CTIGAR: CTIGAR [11] is an adaptation of PDR to software verification.
Our evaluation compares two implementations of CTIGAR, namely VvtCTIGAR from the tool Vvt and our own implementation CPAcheckerCTIGAR. Vvt [20] also provides a configuration that runs a parallel portfolio
combination of Vvt-CTIGAR and bounded model checking, which we call
Vvt-Portfolio.
KI: KI [5] denotes the plain k -induction algorithm without property direction
and without auxiliary invariants, i.e., we configure Alg. 1 such that pd = false
and get_currently_known_invariant() always returns true.
KIPDR: KIPDR denotes a configuration of Alg. 1 such that pd = true
and get_currently_known_invariant() always returns true, i.e., k -induction
with property direction but without additional auxiliary-invariant generation.
KIPDR is, like CTIGAR, an adaptation of PDR to software verification.