|
|
TACAS 2015 |
| Competition on Software Verification (SV-COMP) | |
This web page presents the results of the 2015 4th International Competition on Software Verification (SV-COMP'15).
AProVE1. Termination |
BLAST 2.7.31. DeviceDrivers64 |
Cascade3. MemorySafety |
CBMC1. Floats2. BitVectors 3. Concurrency 3. HeapManipulation 3. Overall |
CPAchecker1. ControlFlow1. MemorySafety 1. Overall 2. Floats 2. Sequentialized 2. Simple 3. BitVectors 3. DeviceDrivers64 |
CPArec3. Recursive |
ESBMC 1.24.11. BitVectors1. Sequentialized 3. ControlFlow 3. Floats |
HIPTNT+3. Termination |
Lazy-CSeq1. Concurrency |
MU-CSeq2. Concurrency |
Predator1. HeapManipulation2. MemorySafety |
SeaHorn1. Simple2. ControlFlow 2. DeviceDrivers64 |
SMACK+Corral1. Arrays1. Recursive 2. HeapManipulation 3. Simple |
Ultimate Automizer2. Recursive2. Termination 2. Overall 3. Arrays 3. Sequentialized |
Ultimate Kojak2. Arrays |
What you can learn from a score-based quantile plot and how to interpret it, is described in the competition report on pages 12 and 13.
Arrays1. SMACK+Corral2. Ultimate Kojak 3. Ultimate Automizer 
|
BitVectors1. ESBMC 1.24.12. CBMC 3. CPAchecker 
|
Concurrency1. Lazy-CSeq2. MU-CSeq 3. CBMC 
|
ControlFlow1. CPAchecker2. SeaHorn 3. ESBMC 1.24.1 
|
DeviceDrivers641. BLAST 2.7.32. SeaHorn 3. CPAchecker 
|
Floats1. CBMC2. CPAchecker 3. ESBMC 1.24.1 
|
HeapManipulation1. Predator2. SMACK+Corral 3. CBMC 
|
MemorySafety1. CPAchecker2. Predator 3. Cascade 
|
Recursive1. SMACK+Corral2. Ultimate Automizer 3. CPArec 
|
Sequentialized1. ESBMC 1.24.12. CPAchecker 3. Ultimate Automizer 
|
Simple1. SeaHorn2. CPAchecker 3. SMACK+Corral 
|
Termination1. AProVE2. Ultimate Automizer 3. HIPTNT+ 
|
Overall1. CPAchecker2. Ultimate Automizer 3. CBMC 
|
||
ControlFlowInteger
|
ECA
|
Loops
|
ProductLines
|
The background color is gold for the winner, silver for the second, and bronze for the third.
In every table cell for competition results, we list the points in the first row and the CPU time (rounded to two significant digits) for successful runs in the second row.
The entry '--' means that the competition candidate opted-out in the category.
The definition of the scoring schema
and the categories is given on the respective SV-COMP web pages.
| Competition candidate | AProVE | Beagle | BLAST 2.7.3 | Cascade | CBMC | CPAchecker | CPArec | ESBMC 1.24.1 | FOREST | Forester | FuncTion | HIPTNT+ | Lazy-CSeq | Map2Check | MU-CSeq | Perentie | Predator | SeaHorn | SMACK+Corral | Ultimate Automizer | Ultimate Kojak | Unbounded Lazy-CSeq |
| Representing Jury Member | Thomas Ströder | Dexi Wang | Vadim Mutilin | Wei Wang | Michael Tautschnig | Matthias Dangl | Ming-Hsien Tsai | Jeremy Morse | Pablo Sánchez | Ondrej Lengal | Caterina Urban | Ton-Chanh Le | Gennaro Parlato | Herbert Oliveira Rocha | Bernd Fischer | Franck Cassez | Tomas Vojnar | Arie Gurfinkel | Zvonimir Rakamaric | Matthias Heizmann | Alexander Nutz | Salvatore La Torre |
| Affiliation | Aachen, Germany | Beijing, China | Moscow, Russia | New York, USA | London, UK | Passau, Germany | Taipei, Taiwan | Bristol, UK | Cantabria, Spain | Brno, Czechia | Paris, France | Singapore, Singapore | Southampton, UK | Manaus, Brazil | Stellenbosch, South Africa | Sydney, Australia | Brno, Czechia | Pittsburgh, USA | Salt Lake City, USA | Freiburg, Germany | Freiburg, Germany | Southampton, UK |
|
Arrays 86 tasks, max. score: 145 |
-- |
-- |
-- |
-- |
-134 2 500 s |
2 62 s |
-- |
-206 5.5 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
0 0.61 s |
48 400 s |
2 6.4 s |
2 5.9 s |
-- |
|
BitVectors 47 tasks, max. score: 83 |
-- |
4 58 s |
-- |
52 16 000 s |
68 1 800 s |
58 870 s |
-- |
69 470 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-80 550 s |
-- |
5 170 s |
-62 120 s |
-- |
|
Concurrency 1 003 tasks, max. score: 1 222 |
-- |
-- |
-- |
-- |
1 039 78 000 s |
0 0 s |
-- |
1 014 13 000 s |
-- |
-- |
-- |
-- |
1 222 5 600 s |
-- |
1 222 16 000 s |
-- |
-- |
- 8 973 42 s |
-- |
-- |
-- |
984 36 000 s |
|
ControlFlow 1 927 tasks, max. score: 3 122 |
-- |
-- |
983 33 000 s |
537 43 000 s |
158 570 000 s |
2 317 47 000 s |
-- |
1 968 59 000 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
2 169 30 000 s |
1 691 78 000 s |
1 887 54 000 s |
872 10 000 s |
-- |
|
ControlFlowInteger 48 tasks, max. score: 78 |
-- |
-- |
51 3 300 s |
38 11 000 s |
62 1 300 s |
77 1 800 s |
-- |
78 87 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
77 440 s |
61 200 s |
78 990 s |
43 1 000 s |
-- |
|
ECA 1 140 tasks, max. score: 1 874 |
-- |
-- |
11 9 800 s |
0 0 s |
- 2 334 560 000 s |
987 39 000 s |
-- |
523 58 000 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
516 25 000 s |
112 45 000 s |
632 46 000 s |
1 14 s |
-- |
|
Loops 142 tasks, max. score: 235 |
-- |
-- |
-14 790 s |
46 32 000 s |
59 4 900 s |
118 2 600 s |
-- |
66 620 s |
168 45 000 s |
-- |
-- |
-- |
-- |
-- |
-- |
125 1 600 s |
-- |
130 1 100 s |
86 370 s |
115 2 900 s |
109 4 300 s |
-- |
|
ProductLines 597 tasks, max. score: 929 |
-- |
-- |
637 19 000 s |
0 0 s |
399 1 900 s |
901 4 100 s |
-- |
917 430 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
913 3 500 s |
917 32 000 s |
554 3 300 s |
87 5 000 s |
-- |
|
DeviceDrivers64 1 650 tasks, max. score: 3 097 |
-- |
-- |
2 736 11 000 s |
-- |
2 293 380 000 s |
2 572 39 000 s |
-- |
2 281 36 000 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
2 657 16 000 s |
2 507 72 000 s |
274 850 s |
82 270 s |
-- |
|
Floats 81 tasks, max. score: 140 |
-- |
-- |
-- |
-- |
129 15 000 s |
78 5 100 s |
-- |
-12 5 300 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-164 5.9 s |
-- |
-- |
-- |
-- |
|
HeapManipulation 80 tasks, max. score: 135 |
-- |
-- |
-- |
70 6 000 s |
100 13 000 s |
96 930 s |
-- |
79 37 s |
-- |
32 1.8 s |
-- |
-- |
-- |
-- |
-- |
-- |
111 140 s |
-37 14 s |
109 820 s |
84 460 s |
84 420 s |
-- |
|
MemorySafety 205 tasks, max. score: 361 |
-- |
-- |
-- |
200 82 000 s |
-433 14 000 s |
326 5 700 s |
-- |
-- |
-- |
22 25 s |
-- |
-- |
-- |
28 2 100 s |
-- |
-- |
221 460 s |
0 0 s |
-- |
95 13 000 s |
66 4 800 s |
-- |
|
Recursive 24 tasks, max. score: 40 |
-- |
6 22 s |
-- |
-- |
0 10 000 s |
16 31 s |
18 140 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-88 2.3 s |
27 2 300 s |
25 310 |
10 220 |
-- |
|
Sequentialized 261 tasks, max. score: 364 |
-- |
-- |
-- |
-- |
-171 39 000 s |
130 11 000 s |
-- |
193 9 600 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-59 5 800 s |
-- |
15 8 600 s |
-10 7 000 s |
-- |
|
Simple 46 tasks, max. score: 68 |
-- |
-- |
32 4 200 s |
-- |
51 16 000 s |
54 4 000 s |
-- |
29 990 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
65 1 400 s |
51 5 100 s |
0 1 800 s |
3 140 s |
-- |
|
Termination 393 tasks, max. score: 742 |
610 5 400 s |
-- |
-- |
-- |
-- |
0 0 s |
-- |
-- |
-- |
-- |
350 61 s |
545 300 s |
-- |
-- |
-- |
-- |
-- |
0 0 s |
-- |
565 8 600 s |
-- |
-- |
|
Overall 5 803 tasks, max. score: 9 562 |
-- |
-- |
-- |
-- |
1 731 1 100 000 s |
4 889 110 000 s |
-- |
- 2 161 130 000 s |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
-- |
- 6 228 53 000 s |
-- |
2 301 87 000 s |
231 23 000 s |
-- |
Note on meta-categories: The score is not the sum of scores of the sub-categories (normalization). The run time is the sum of run times of the sub-categories, rounded to two significant digits.
The raw data of the competition are publicly available.
If you did not find what you are looking for, please do not hesitate to contact me (Dirk Beyer, Competition Chair).