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

Results of the Competition

This web page presents the results of the 2012 International Competition on Software Verification (SVCOMP'12). The benchmarks and rules are described on the competition web site or in the competition report.

All Results

In every table cell for competition results, we list the points in the first row and the CPU time for successful runs in the second row. The background color is gold for the winner, silver for the second, and bronze for the third.

The entry '--' means that the competition candidate opted-out or obtained a total of less than 0 points in the category.

Competition candidate BLAST 2.7 CPAchecker-ABE 1.0.10 CPAchecker-Memo 1.0.10 ESBMC 1.17 FShell 1.3 LLBMC 0.9 Predator 2011-10-11 QARMC-HSF SATabs 3.0 Wolverine 0.5c
Representing Jury Member Vadim Mutilin Philipp Wendler Daniel Wonisch Bernd Fischer Helmut Veith Carsten Sinz Tomas Vojnar Andrey Rybalchenko Michael Tautschnig Georg Weissenbacher
Affiliation Moscow, Russia Passau, Germany Paderborn, Germany Southampton, UK Vienna, Austria Karlsruhe, Germany Brno, Czechia Munich, Germany Oxford, UK Princeton, USA
ControlFlowInteger
93 files, max score: 144 		71
9900 s 		141
1000 s 		140
3200 s 		102
4500 s 		28
580 s 		100
2400 s 		17
1100 s 		140
4800 s 		75
5400 s 		39
580 s
DeviceDrivers
59 files, max score: 103 		72
30 s 		51
97 s 		51
93 s 		63
160 s 		20
3.5 s 		80
1.6 s 		80
1.9 s 		--
71
140 s 		68
65 s
DeviceDrivers64
41 files, max score: 66 		55
1400 s 		26
1900 s 		49
500 s 		10
870 s 		0
0 s 		1
110 s 		0
0 s 		--
32
3200 s 		16
1300 s
HeapManipulation
14 files, max score: 24 		--
4
16 s 		4
16 s 		1
220 s 		--
17
210 s 		20
1.0 s 		--
--
--
SystemC
62 files, max score: 87 		33
4000 s 		45
1100 s 		36
450 s 		67
760 s 		--
8
2.4 s 		21
630 s 		8
820 s 		57
5000 s 		36
1900 s
Concurrency
8 files, max score: 11
 --
0
0 s 		0
0 s 		6
270 s 		0
0 s 		--
0
0 s 		--
1
1.4 s 		--
Overall
277 files, max score: 435 		231
15000 s 		267
4100 s 		280
4300 s 		249
6800 s 		48
580 s 		206
2700 s 		138
1700 s 		148
5600 s 		236
14000 s 		159
3800 s

Ranking by Category

ControlFlowInteger

1. CPAchecker-ABE 1.0.10
2. CPAchecker-Memo 1.0.10
3. QARMC-HSF
4. ESBMC 1.17
5. LLBMC 0.9

DeviceDrivers

1. LLBMC 0.9
2. Predator
3. BLAST 2.7
4. SATabs 3.0
5. Wolverine 0.5c

DeviceDrivers64

1. BLAST 2.7
2. CPAchecker-Memo 1.0.10
3. SATabs 3.0
4. CPAchecker-ABE 1.0.10
5. Wolverine 0.5c

HeapManipulation

1. Predator
2. LLBMC 0.9
3. CPAchecker-ABE 1.0.10
3. CPAchecker-Memo 1.0.10
5. ESBMC 1.17

SystemC

1. ESBMC 1.17
2. SATabs 3.0
3. CPAchecker-ABE 1.0.10
4. CPAchecker-Memo 1.0.10
5. Wolverine 0.5c

Concurrency

1. ESBMC 1.17
2. SATabs 3.0
3. --
4. --
5. --

Overall

1. CPAchecker-Memo 1.0.10
2. CPAchecker-ABE 1.0.10
3. ESBMC 1.17
4. SATabs 3.0
5. BLAST 2.7

Placements by Tool

BLAST 2.7

  • Winner in DeviceDrivers64
  • Bronze in DeviceDrivers

CPAchecker-ABE 1.0.10

  • Winner in ControlFlowInteger
  • Silver in Overall
  • Bronze in SystemC
  • Bronze in HeapManipulation

CPAchecker-Memo 1.0.10

  • Winner in Overall
  • Silver in ControlFlowInteger
  • Silver in DeviceDrivers64
  • Bronze in HeapManipulation

ESBMC 1.17

  • Winner in SystemC
  • Winner in Concurrency
  • Bronze in Overall

LLBMC 0.9

  • Winner in DeviceDrivers
  • Silver in HeapManipulation

Predator

  • Winner in HeapManipulation
  • Silver in DeviceDrivers

QARMC-HSF

  • Bronze in ControlFlowInteger

SATabs 3.0

  • Silver in SystemC
  • Silver in Concurrency
  • Bronze in DeviceDrivers64