Software Verification with PDR: An Implementation of the State of the Art
17
Table 3: Results of SV-COMP 2019 for the six verifiers that performed best
on our seven manually crafted verification tasks, compared to the results of
KI
←−KIPDR approach previously shown in Table 2; an entry “T” means that
the CPU-time limit was exceeded, an entry “M” means that the memory limit
was exceeded, an entry “O” means that the verifier gave up deliberately for other
reasons, and all other entries represent the CPU time a verifier configuration
spent to correctly solve the task; note that SV-COMP 2019 used Ubuntu 18.04
based on Linux 4.15, whereas our evaluation of KI
←−KIPDR used Ubuntu 16.04
based on Linux 4.4; otherwise, the evaluation environment was the same
Task
SV-COMP 2019
KI
←−KIPDR
Skink UAutomizer UKojak UTaipan VeriAbs VIAP
const.c
4.2 s
8.7 s
9.1 s
8.2 s
13 s 110 s
3.8 s
eq1.c
290 s
7.8 s
7.6 s
8.3 s
14 s 57 s
4.9 s
eq2.c
4.1 s
8.1 s
8.6 s
7.6 s
14 s
4.7 s
3.9 s
even.c
3.7 s
7.4 s
8.2 s
8.6 s 140 s
4.5 s
3.9 s
odd.c
O
9.6 s
T
11 s 140 s
4.6 s
4.1 s
mod4.c
4.0 s
8.4 s
8.4 s
7.7 s 140 s
4.5 s
3.6 s
bin-suffix-5.c
O
14 s
T
13 s
13 s
4.7 s
3.6 s
Ultimate Taipan, VeriAbs, and VIAP. Fig. 4a directly compares the CPU times
spent on tasks of in the subcategory ReachSafety-Loops, which is known to contain
many tasks that require effort to be spent on generating loop invariants, by both
VeriAbs, which was the best verifier in that subcategory, and KI
←−KIPDR.
We observe that for the majority of tasks that were solved by both verifiers,
KI
←−KIPDR is faster than VeriAbs, often by more than an order of magnitude.
This shows that the invariant generator KIPDR can be significantly faster than
other approaches, depending on the benchmark set. As before, a more in-depth
discussion can be found in the technical report [8].
Comparison against PDR-Based Verification Tools. The last three
columns of Table 1 give an overview over the best configurations of three
software verifiers that use adaptations of PDR: For CPAchecker, we selected
KI
←−DF;KIPDR. For SeaHorn, we used the same configuration as submitted by the developers to the 2016 Competition on Software Verification (SVCOMP 2016) [22]. For Vvt, we used the portfolio configuration. We observe that
SeaHorn achieves the highest number of correct proofs, but also has a significant
amount of incorrect proofs. CPAchecker is the slowest of the three tools and
finds fewer proofs than SeaHorn, but CPAchecker has no wrong proofs, and
also closely leads in the amount of found bugs. The score-based quantile plot
of these results displayed in Fig. 4b visualizes the effects of incorrect results on
the computed score. While the graph for SeaHorn is longer, i.e., shows that it
solved the most tasks, it is offset to the left by a total penalty of −3 344 points,
such that in the end, KI
←−DF;KIPDR accumulates the highest score because
it has a smaller penalty of only −32 points.
17
Table 3: Results of SV-COMP 2019 for the six verifiers that performed best
on our seven manually crafted verification tasks, compared to the results of
KI
←−KIPDR approach previously shown in Table 2; an entry “T” means that
the CPU-time limit was exceeded, an entry “M” means that the memory limit
was exceeded, an entry “O” means that the verifier gave up deliberately for other
reasons, and all other entries represent the CPU time a verifier configuration
spent to correctly solve the task; note that SV-COMP 2019 used Ubuntu 18.04
based on Linux 4.15, whereas our evaluation of KI
←−KIPDR used Ubuntu 16.04
based on Linux 4.4; otherwise, the evaluation environment was the same
Task
SV-COMP 2019
KI
←−KIPDR
Skink UAutomizer UKojak UTaipan VeriAbs VIAP
const.c
4.2 s
8.7 s
9.1 s
8.2 s
13 s 110 s
3.8 s
eq1.c
290 s
7.8 s
7.6 s
8.3 s
14 s 57 s
4.9 s
eq2.c
4.1 s
8.1 s
8.6 s
7.6 s
14 s
4.7 s
3.9 s
even.c
3.7 s
7.4 s
8.2 s
8.6 s 140 s
4.5 s
3.9 s
odd.c
O
9.6 s
T
11 s 140 s
4.6 s
4.1 s
mod4.c
4.0 s
8.4 s
8.4 s
7.7 s 140 s
4.5 s
3.6 s
bin-suffix-5.c
O
14 s
T
13 s
13 s
4.7 s
3.6 s
Ultimate Taipan, VeriAbs, and VIAP. Fig. 4a directly compares the CPU times
spent on tasks of in the subcategory ReachSafety-Loops, which is known to contain
many tasks that require effort to be spent on generating loop invariants, by both
VeriAbs, which was the best verifier in that subcategory, and KI
←−KIPDR.
We observe that for the majority of tasks that were solved by both verifiers,
KI
←−KIPDR is faster than VeriAbs, often by more than an order of magnitude.
This shows that the invariant generator KIPDR can be significantly faster than
other approaches, depending on the benchmark set. As before, a more in-depth
discussion can be found in the technical report [8].
Comparison against PDR-Based Verification Tools. The last three
columns of Table 1 give an overview over the best configurations of three
software verifiers that use adaptations of PDR: For CPAchecker, we selected
KI
←−DF;KIPDR. For SeaHorn, we used the same configuration as submitted by the developers to the 2016 Competition on Software Verification (SVCOMP 2016) [22]. For Vvt, we used the portfolio configuration. We observe that
SeaHorn achieves the highest number of correct proofs, but also has a significant
amount of incorrect proofs. CPAchecker is the slowest of the three tools and
finds fewer proofs than SeaHorn, but CPAchecker has no wrong proofs, and
also closely leads in the amount of found bugs. The score-based quantile plot
of these results displayed in Fig. 4b visualizes the effects of incorrect results on
the computed score. While the graph for SeaHorn is longer, i.e., shows that it
solved the most tasks, it is offset to the left by a total penalty of −3 344 points,
such that in the end, KI
←−DF;KIPDR accumulates the highest score because
it has a smaller penalty of only −32 points.