16
D. Beyer and M. Dangl
1
10
100
1 000
CPU time (s)
CPAchecker-CTIGAR
Vvt-CTIGAR
0
200
400
600
800
1 000
1 200
0
n-th fastest correct result (proof or alarm)
Fig. 3: Comparing two implementations of CTIGAR; quantile plot for accumulated
number of solved tasks (proofs and alarms) showing the CPU time (linear scale
below 1 s, logarithmic above) for the successful results of CPAchecker-CTIGAR
and Vvt-CTIGAR
Table 2: Results of four k -induction-based configurations in CPAchecker with
different approaches for generating auxiliary invariants for seven manually crafted
verification tasks that do not contain bugs and are not solved by k -induction
without auxiliary invariants; an entry “T” means that the CPU-time limit was
exceeded, an entry “M” means that the memory limit was exceeded, and all other
entries represent the CPU time a configuration spent to correctly solve the task
Task
KI←DF
KI
←−KIPDR
Boxes
Boxes,
Eq
Boxes,
Eq,
Mod2
const.c
3.3 s
3.3 s
3.2 s
3.8 s
eq1.c
T
3.2 s
3.3 s
4.9 s
eq2.c
M
M
M
3.9 s
even.c
T
T
3.5 s
3.9 s
odd.c
T
T
3.4 s
4.1 s
mod4.c
T
T
T
3.6 s
bin-suffix-5.c M
M
M
3.6 s
Comparison with Non-PDR Approaches. The seven example programs
8
were added to the benchmark collection that was also used for SV-COMP 2019, and
thus, results are available for all verifiers that participated in the competition
9
.
Table 3 summarizes the results of the best six verifiers in comparison with
the KI
←−KIPDR approach that we created for the study in this paper. Those
verifiers are, in alphabetical order, Skink, Ultimate Automizer, Ultimate Kojak,
8 https://github.com/sosy-lab/sv-benchmarks/tree/svcomp19/c/loop-invariants/
9 See the last seven rows in this table: https://sv-comp.sosy-lab.org/2019/results/
results-verified/ReachSafety-Loops.table.html
D. Beyer and M. Dangl
1
10
100
1 000
CPU time (s)
CPAchecker-CTIGAR
Vvt-CTIGAR
0
200
400
600
800
1 000
1 200
0
n-th fastest correct result (proof or alarm)
Fig. 3: Comparing two implementations of CTIGAR; quantile plot for accumulated
number of solved tasks (proofs and alarms) showing the CPU time (linear scale
below 1 s, logarithmic above) for the successful results of CPAchecker-CTIGAR
and Vvt-CTIGAR
Table 2: Results of four k -induction-based configurations in CPAchecker with
different approaches for generating auxiliary invariants for seven manually crafted
verification tasks that do not contain bugs and are not solved by k -induction
without auxiliary invariants; an entry “T” means that the CPU-time limit was
exceeded, an entry “M” means that the memory limit was exceeded, and all other
entries represent the CPU time a configuration spent to correctly solve the task
Task
KI←DF
KI
←−KIPDR
Boxes
Boxes,
Eq
Boxes,
Eq,
Mod2
const.c
3.3 s
3.3 s
3.2 s
3.8 s
eq1.c
T
3.2 s
3.3 s
4.9 s
eq2.c
M
M
M
3.9 s
even.c
T
T
3.5 s
3.9 s
odd.c
T
T
3.4 s
4.1 s
mod4.c
T
T
T
3.6 s
bin-suffix-5.c M
M
M
3.6 s
Comparison with Non-PDR Approaches. The seven example programs
8
were added to the benchmark collection that was also used for SV-COMP 2019, and
thus, results are available for all verifiers that participated in the competition
9
.
Table 3 summarizes the results of the best six verifiers in comparison with
the KI
←−KIPDR approach that we created for the study in this paper. Those
verifiers are, in alphabetical order, Skink, Ultimate Automizer, Ultimate Kojak,
8 https://github.com/sosy-lab/sv-benchmarks/tree/svcomp19/c/loop-invariants/
9 See the last seven rows in this table: https://sv-comp.sosy-lab.org/2019/results/
results-verified/ReachSafety-Loops.table.html