TACAS Logo TACAS 2015
Competition on Software Verification (SV-COMP)

Results of the Competition

This web page presents the results of the 2015 4th International Competition on Software Verification (SV-COMP'15).


Placements by Tool

AProVE

1. Termination

BLAST 2.7.3

1. DeviceDrivers64

Cascade

3. MemorySafety

CBMC

1. Floats
2. BitVectors
3. Concurrency
3. HeapManipulation
3. Overall

CPAchecker

1. ControlFlow
1. MemorySafety
1. Overall
2. Floats
2. Sequentialized
2. Simple
3. BitVectors
3. DeviceDrivers64

CPArec

3. Recursive

ESBMC 1.24.1

1. BitVectors
1. Sequentialized
3. ControlFlow
3. Floats

HIPTNT+

3. Termination

Lazy-CSeq

1. Concurrency

MU-CSeq

2. Concurrency

Predator

1. HeapManipulation
2. MemorySafety

SeaHorn

1. Simple
2. ControlFlow
2. DeviceDrivers64

SMACK+Corral

1. Arrays
1. Recursive
2. HeapManipulation
3. Simple

Ultimate Automizer

2. Recursive
2. Termination
2. Overall
3. Arrays
3. Sequentialized

Ultimate Kojak

2. Arrays

Ranking by Category (with Score-Based Quantile Plots)

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.

Arrays

1. SMACK+Corral
2. Ultimate Kojak
3. Ultimate Automizer

BitVectors

1. ESBMC 1.24.1
2. CBMC
3. CPAchecker

Concurrency

1. Lazy-CSeq
2. MU-CSeq
3. CBMC

ControlFlow

1. CPAchecker
2. SeaHorn
3. ESBMC 1.24.1

DeviceDrivers64

1. BLAST 2.7.3
2. SeaHorn
3. CPAchecker

Floats

1. CBMC
2. CPAchecker
3. ESBMC 1.24.1

HeapManipulation

1. Predator
2. SMACK+Corral
3. CBMC

MemorySafety

1. CPAchecker
2. Predator
3. Cascade

Recursive

1. SMACK+Corral
2. Ultimate Automizer
3. CPArec

Sequentialized

1. ESBMC 1.24.1
2. CPAchecker
3. Ultimate Automizer

Simple

1. SeaHorn
2. CPAchecker
3. SMACK+Corral

Termination

1. AProVE
2. Ultimate Automizer
3. HIPTNT+

Overall

1. CPAchecker
2. Ultimate Automizer
3. CBMC

Quantile Plots for Sub-Categories of Category ControlFlowAndIntegerVariables:

ControlFlowInteger

ECA

Loops

ProductLines


Table of All Results

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.