Software Verification with PDR: An Implementation of the State of the Art
15
Table 1: Results for all 5 591 verification tasks, 1 457 of which contain bugs, while
the other 4 134 are considered to be safe, for the two CTIGAR implementations
CPAchecker-CTIGAR and Vvt-CTIGAR, for a theoretical “virtual best” combination of both CTIGAR implementations where an oracle selects the best
implementation for each task, for k -induction without auxiliary invariants (KI),
and for the best configurations of each tool: CPAchecker’s KI
←−DF;KIPDR,
SeaHorn, and Vvt as a portfolio verifier.
Verifier
CTIGAR
KI
Best of each tool
CPAchecker
Vvt
KI
←−DF;
KIPDR
SeaHorn
Vvt -
Portfolio
Score
1 903
879
3 282
5 398
2 848
727
Correct results
1 087
739
2 075
3 095
3 468
839
Correct proofs
832
524
1 239
2 335
2 724
528
Correct alarms
255
215
836
760
744
311
Wrong proofs
0
5
0
0
46
9
Wrong alarms
1
1 4
2
2
117
22
Timeouts
3 982
110
2 764
2 006
1 476
524
Out of memory
23
28
315
243
231
22
Other inconclusive
498
4 695
435
245
253
4 175
Times for correct results
Total CPU Time (h)
9.0
3 .2
30
54
29
5.7
Mean CPU Time (s)
30
16
52
63
31
25
Median CPU Time (s)
4.9
0 .24
9.8
10
0.89
0.45
Suitability of CPAchecker for PDR. The first set of experiments showed
that our implementation is at least as good as (and even better than) the only
available implementation of PDR for software model checking. Columns two and
three of Table 1 compare the results obtained by running the two implementations
of CTIGAR on the whole benchmark set, and the last column of the table shows
the results achieved with the standard configuration of Vvt, which runs not only
CTIGAR, but a portfolio analysis of CTIGAR and bounded model checking. The
quantile plot in Fig. 3 shows the CPU times that the two tool configurations
spent on their correct results.
KIPDR versus Data-Flow Techniques. Data-flow-based techniques are usually more efficient than KIPDR. The higher efficiency of data-flow-based techniques is most likely due to the simple form of the invariants needed to prove
the programs correct. In order to experiment with progams that have some more
interesting invariants, we created a few programs by hand and tried to verify
those. Table 2 shows the results we obtained for these tasks. Our experiments
support the hypothesis that KIPDR can be very strong and efficient on tasks
that other approaches can not solve. It is important to note that this is an ‘exists’
statement and can not be generalized, as shown by the results that KIPDR is
often outperformed by simpler, data-flow-based invariant-generation techniques.
15
Table 1: Results for all 5 591 verification tasks, 1 457 of which contain bugs, while
the other 4 134 are considered to be safe, for the two CTIGAR implementations
CPAchecker-CTIGAR and Vvt-CTIGAR, for a theoretical “virtual best” combination of both CTIGAR implementations where an oracle selects the best
implementation for each task, for k -induction without auxiliary invariants (KI),
and for the best configurations of each tool: CPAchecker’s KI
←−DF;KIPDR,
SeaHorn, and Vvt as a portfolio verifier.
Verifier
CTIGAR
KI
Best of each tool
CPAchecker
Vvt
KI
←−DF;
KIPDR
SeaHorn
Vvt -
Portfolio
Score
1 903
879
3 282
5 398
2 848
727
Correct results
1 087
739
2 075
3 095
3 468
839
Correct proofs
832
524
1 239
2 335
2 724
528
Correct alarms
255
215
836
760
744
311
Wrong proofs
0
5
0
0
46
9
Wrong alarms
1
1 4
2
2
117
22
Timeouts
3 982
110
2 764
2 006
1 476
524
Out of memory
23
28
315
243
231
22
Other inconclusive
498
4 695
435
245
253
4 175
Times for correct results
Total CPU Time (h)
9.0
3 .2
30
54
29
5.7
Mean CPU Time (s)
30
16
52
63
31
25
Median CPU Time (s)
4.9
0 .24
9.8
10
0.89
0.45
Suitability of CPAchecker for PDR. The first set of experiments showed
that our implementation is at least as good as (and even better than) the only
available implementation of PDR for software model checking. Columns two and
three of Table 1 compare the results obtained by running the two implementations
of CTIGAR on the whole benchmark set, and the last column of the table shows
the results achieved with the standard configuration of Vvt, which runs not only
CTIGAR, but a portfolio analysis of CTIGAR and bounded model checking. The
quantile plot in Fig. 3 shows the CPU times that the two tool configurations
spent on their correct results.
KIPDR versus Data-Flow Techniques. Data-flow-based techniques are usually more efficient than KIPDR. The higher efficiency of data-flow-based techniques is most likely due to the simple form of the invariants needed to prove
the programs correct. In order to experiment with progams that have some more
interesting invariants, we created a few programs by hand and tried to verify
those. Table 2 shows the results we obtained for these tasks. Our experiments
support the hypothesis that KIPDR can be very strong and efficient on tasks
that other approaches can not solve. It is important to note that this is an ‘exists’
statement and can not be generalized, as shown by the results that KIPDR is
often outperformed by simpler, data-flow-based invariant-generation techniques.