18
D. Beyer and M. Dangl
.01
.1
1
10
100
1 000
.01
.1
1
10
100
1 000
CPU time for VeriAbs (s)
CPU time for KI
←−KIPDR (s)
(a) Scatter plot comparing the CPU
times spent on tasks by VeriAbs and
KI
←−KIPDR
1
10
100
1 000
CPU time (s)
KI
←−DF;KIPDR
SeaHorn
Vvt-Portfolio
−2 000
0
2 000
4 000
0
Accumulated score
(b) Quantile plot for accumulated score of
solved tasks (offset to the left by total penalty
from wrong results) showing the CPU time
(linear scale below 1 s, logarithmic above) for
the successful results of KI
←−DF;KIPDR, SeaHorn, and Vvt-Portfolio
Fig. 4: Plots that support the claim that the conclusions of the evaluation are
relevant
These results confirm our hypothesis that our previous conclusions are relevant,
because they are supported by an implementation that is competitive when
compared to the best available PDR-based tool implementations.
5 Conclusion
Property-directed reachability (a.k.a. IC3) is a verification approach that is popular and successful in some fields of formal verification (e.g., hardware designs,
Horn clauses). Unfortunately, there is a large gap between this success story and
the applicability in practical software verification. We are closing this gap by
(a) providing a well-engineered implementation of one published adaptation of
PDR to software verification, (b) designing and implementing an invariant generator based on the ideas of PDR, and (c) providing an evaluation of all applicable
tools and approaches on the largest available benchmark set of C verification tasks.
This provides a good foundation as baseline for ongoing research in this area.
The results of our comparative evaluation extend the knowledge about PDR for
software verification in the following ways: (1) Our implementation outperforms
the existing implementation of PDR (Vvt) and is more precise than the other
software verifier that uses PDR (SeaHorn). Thus, our implementation can serve as
a reference implementation for further research on PDR for software verification.
(2) On most of the programs in the widely used sv-benchmarks collection of
verification tasks, other techniques are more effective (solve more problems)
and more efficient (solve the problems faster). (3) PDR can be an effective and
efficient technique for computing invariants that are difficult to obtain: there
are programs for which our PDR-based approach is more efficient than the best
invariant generator from SV-COMP in the subcategory ReachSafety-Loops.
D. Beyer and M. Dangl
.01
.1
1
10
100
1 000
.01
.1
1
10
100
1 000
CPU time for VeriAbs (s)
CPU time for KI
←−KIPDR (s)
(a) Scatter plot comparing the CPU
times spent on tasks by VeriAbs and
KI
←−KIPDR
1
10
100
1 000
CPU time (s)
KI
←−DF;KIPDR
SeaHorn
Vvt-Portfolio
−2 000
0
2 000
4 000
0
Accumulated score
(b) Quantile plot for accumulated score of
solved tasks (offset to the left by total penalty
from wrong results) showing the CPU time
(linear scale below 1 s, logarithmic above) for
the successful results of KI
←−DF;KIPDR, SeaHorn, and Vvt-Portfolio
Fig. 4: Plots that support the claim that the conclusions of the evaluation are
relevant
These results confirm our hypothesis that our previous conclusions are relevant,
because they are supported by an implementation that is competitive when
compared to the best available PDR-based tool implementations.
5 Conclusion
Property-directed reachability (a.k.a. IC3) is a verification approach that is popular and successful in some fields of formal verification (e.g., hardware designs,
Horn clauses). Unfortunately, there is a large gap between this success story and
the applicability in practical software verification. We are closing this gap by
(a) providing a well-engineered implementation of one published adaptation of
PDR to software verification, (b) designing and implementing an invariant generator based on the ideas of PDR, and (c) providing an evaluation of all applicable
tools and approaches on the largest available benchmark set of C verification tasks.
This provides a good foundation as baseline for ongoing research in this area.
The results of our comparative evaluation extend the knowledge about PDR for
software verification in the following ways: (1) Our implementation outperforms
the existing implementation of PDR (Vvt) and is more precise than the other
software verifier that uses PDR (SeaHorn). Thus, our implementation can serve as
a reference implementation for further research on PDR for software verification.
(2) On most of the programs in the widely used sv-benchmarks collection of
verification tasks, other techniques are more effective (solve more problems)
and more efficient (solve the problems faster). (3) PDR can be an effective and
efficient technique for computing invariants that are difficult to obtain: there
are programs for which our PDR-based approach is more efficient than the best
invariant generator from SV-COMP in the subcategory ReachSafety-Loops.