TACAS 2017
6th Competition on Software Verification (SV-COMP)

Results of the Competition

This web page presents the results of the 2017 6th International Competition on Software Verification (SV-COMP '17).

• The competition report describes the competition and the results in more detail.
• The benchmarks and rules are also available from the competition web site.

The background color is gold for the winner, silver for the second, and bronze for the third.

Here some brief directions for reading the score-based quantile plots:

• The right end of the graph displays the achieved score. The score is SV-COMP's definition of quality. You can read the ranking on the top from right to left.
• The left end of the graph displays the amount of wrong results that a verifier produced. Left-most start means worst.
• The length of the graph displays the amount of correct verification work. Long is good.
• More is described here.

Here some brief directions for navigating in the BenchExec-generated tables with the results:

• Please note the header with the menu "Select Columns, Filter Rows, etc.", which loads only after all data are retrieved from the server.
• The tables contain all information that I thought you could be interested in. If there are too many columns, you can get rid of some with "Select Columns". You can also investigate special classes of rows using "Filter Rows".
• If you want to see more data, including the time and memory needed for witness validation, please click on the score value in a table cell (works only for base categories). In those tables, there is also a link available to get the witness that the verifier generated.
• In all results tables, the sources of the verification task is available via click on the name of the verification task. The log files are available via click on the status (result).
• If you want to investigate even more, you can download the raw data that I obtained with BenchExec and from which I compiled all the tables and aggregated data displays. For the most detailed tables, which end on ".xml.bz2.table.html", you can obtain the raw data by accessing the URL with the ".table.html" removed.
• Falsification: Here only bug hunting matters and proof generation is ignored. There are no different results tables for the Falsification category because all verification tasks (except Termination) are included, but the TRUE results are ignored (no score assigned). If you want to remove for a particular verifier the TRUE results, proceed as follows: Click in the menu on "Filter Rows". Then select "status" for the verifier you are interested in for row selection, then a choose box with all the status-values appears. There you choose "true" and then click "invert filter".
• More on table generation is described here.
• Column "score" shows the (not normalized) score assigned to the result of the verification task.
• Column "witness" contains a link to the witness file for download/display.
• Column "inspect witness" opens a new page that displays information about the witness an a list of witnesses that other verifiers produced for the same program.
• Column "cpu" shows the consumed CPU time.
• Column "wall" shows the elapsed wall time.
• Column "energy" shows the energy consumed by the CPU.
• Column "mem" shows the peak memory usage.
• Column "blkio-w" shows the accumulated amount of information written to block devices.
• Column "blkio-r" shows the accumulated amount of information read from block devices.
• More information on results.

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.

ReachSafety 1. SMACK 2. CPA-Seq 3. UAutomizer	MemSafety 1. PredatorHP 2. UAutomizer 3. Symbiotic	ConcurrencySafety 1. Yogar-CBMC 2. Lazy-CSeq-Abs 3. Lazy-CSeq-Swarm
Overflows 1. SMACK 2. UAutomizer 3. UTaipan	Termination 1. UAutomizer 2. AProVE 3. CPA-Seq	SoftwareSystems 1. SMACK 2. UTaipan 3. UAutomizer
FalsificationOverall 1. CBMC 2. ESBMC-kind 3. ESBMC-incr	Overall 1. UAutomizer 2. SMACK 3. CPA-Seq

Table of All Results

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.

Hide base categories

Verifiers	Plots	2LS	AProVE	BLAST	CBMC	Ceagle	CIVL	ConSequence	CPA-BAM-BnB	CPA-kInd	CPA-Seq	DepthK	ESBMC	ESBMC-falsi	ESBMC-incr	ESBMC-kind	Forester	HipTNT+	Lazy-CSeq	Lazy-CSeq-Abs	Lazy-CSeq-Swarm	MU-CSeq	PredatorHP	Skink	SMACK	Symbiotic	SymDIVINE	UAutomizer	UKojak	UL-CSeq	UTaipan	VeriAbs	Yogar-CBMC
Representing Jury Member		Peter Schrammel	Jera Hensel	Vadim Mutilin	Michael Tautschnig	Guang Chen	Stephen Siegel	Anand Yeolekar	Pavel Andrianov	Matthias Dangl	Karlheinz Friedberger	Herbert Oliveira Rocha	Lucas Cordeiro	Bernd Fischer	Denis Nicole	Mikhail Ramalho	Martin Hruska	Ton Chanh Le	Omar Inverso	Bernd Fischer	Truc Nguyen Lam	Salvatore La Torre	Tomas Vojnar	Franck Cassez	Zvonimir Rakamaric	Jan Strejček	Jiří Barnat	Matthias Heizmann	Daniel Dietsch	Gennaro Parlato	Marius Greitschus	Priyanka Darke	Liangze Yin
Affiliation		University of Sussex, UK	RWTH Aachen, Germany	ISP RAS, Russia	Queen Mary, UK	Tsinghua University, China	University of Delaware, USA	TCS, India	ISP RAS, Russia	University of Passau, Germany	University of Passau, Germany	Federal University of Roraima, Brazil	University of Oxford, UK	Stellenbosch University, ZA	University of Southampton, UK	University of Southampton, UK	Brno University of Technology, Czechia	National University of Singapore, Singapore	Gran Sasso Science Institute, Italy	Stellenbosch University, ZA	University of Southampton, UK	University of Salerno, Italy	Brno University of Technology, Czechia	Macquarie University at Sydney, Australia	University of Utah, USA	Masaryk University, Czechia	Masaryk University, Czechia	University of Freiburg, Germany	University of Freiburg, Germany	University of Southampton, UK	University of Freiburg, Germany	TCS, India	National University of Defense Technology, China
ReachSafety 2897 tasks, max. score: 4696		1038			2154	2170				2156	2862	1552	1125	583	1810	1940									3432	2063		2372	1564		1894
CPU time		81000 s			32000 s	20000 s				63000 s	140000 s	84000 s	93000 s	27000 s	42000 s	27000 s									360000 s	10000 s		97000 s	64000 s		45000 s
ReachSafety-Arrays 135 tasks, max. score: 230		-10			30	214			-104	8	9	6	48	6	36	30									212	145		22	17		13	162
CPU time		1200 s			1200 s	85 s			210 s	230 s	1400 s	3000 s	23000 s	7.5 s	490 s	660 s									8800 s	260 s		1300 s	1300 s		210 s	45000 s
ReachSafety-BitVectors 50 tasks, max. score: 86		54			57	76			-150	67	75	54	46	10	48	53								12	78	50		56	27		43
CPU time		110 s			460 s	200 s			330 s	1800 s	1700 s	3900 s	8100 s	15 s	510 s	640 s								39 s	11000 s	780 s		2200 s	710 s		1100 s
ReachSafety-ControlFlow 94 tasks, max. score: 146		44			58	9			-180	89	112	64	27	35	51	80									125	52	62	95	47		75	33
CPU time		1200 s			200 s	3000 s			1300 s	1300 s	3100 s	4900 s	830 s	5300 s	8100 s	9200 s									14000 s	8.9 s	3700 s	2900 s	4500 s		3200 s	4700 s
ReachSafety-ECA 1149 tasks, max. score: 1887		644			143	1474			631	790	1088	3	56	112	111	82									242	93	-145	861	593		96	405
CPU time		58000 s			24000 s	550 s			31000 s	26000 s	86000 s	510 s	25000 s	17000 s	26000 s	7000 s									92000 s	8400 s	4400 s	67000 s	46000 s		12000 s	140000 s
ReachSafety-Floats 172 tasks, max. score: 314		248			264	298			-56	107	129	100	308	18	194	173									153	86		109	62		109
CPU time		6400 s			3000 s	15000 s			1400 s	5700 s	4100 s	3800 s	5200 s	2400 s	5100 s	3300 s									5400 s	19 s		5900 s	490 s		6400 s
ReachSafety-Heap 173 tasks, max. score: 280		-370			186	69			-160	171	157	184	135	63	184	148	139						197		272	208		193	152		177
CPU time		24 s			98 s	2.8 s			720 s	780 s	1600 s	670 s	350 s	670 s	39 s	44 s	1200 s						85 s		29000 s	29 s		3400 s	2400 s		2600 s
ReachSafety-Loops 156 tasks, max. score: 261		145			107	33			115	151	157	120	-295	36	96	118								98	194	136	60	156	147		162	194
CPU time		550 s			500 s	910 s			1400 s	2300 s	5100 s	3400 s	4500 s	390 s	190 s	1100 s								1900 s	25000 s	29 s	330 s	1800 s	3100 s		3100 s	8000 s
ReachSafety-ProductLines 597 tasks, max. score: 929		772			393	134			657	660	920	393	623	129	317	437									920	453	-592	618	487		562	634
CPU time		8700 s			2300 s	10 s			4300 s	3800 s	5800 s	50000 s	21000 s	25 s	230 s	1800 s									160000 s	200 s	3700 s	5200 s	3600 s		9500 s	88000 s
ReachSafety-Recursive 98 tasks, max. score: 151		0			86	43			19	10	119	35	72	37	89	89									125	91	57	116	65		100	45
CPU time		0 s			25 s	5.8 s			28 s	22 s	390 s	47 s	1200 s	6.6 s	520 s	1000 s									8400 s	8.6 s	14 s	1800 s	670 s		4100 s	170 s
ReachSafety-Sequentialized 273 tasks, max. score: 376		6			136	0			0	170	206	33	-51	1	37	64									179	41	-191	48	15		12	-26
CPU time		5000 s			230 s	0 s			2000 s	21000 s	32000 s	14000 s	4900 s	210 s	620 s	1900 s									12000 s	350 s	4700 s	5200 s	1600 s		2400 s	5800 s
MemSafety 328 tasks, max. score: 541		-918			219	138				0	88	27	-85	-65	80	191							319		150	304		308	268		296
CPU time		440 s			1900 s	2.5 s				0 s	1600 s	8600 s	12000 s	4500 s	9600 s	4800 s							2900 s		79000 s	280 s		6800 s	7600 s		8300 s
MemSafety-Arrays 69 tasks, max. score: 117		-440			18	116			0	0	6	20	-39	18	18	18							7		82	83		86	64		84
CPU time		4.6 s			3.8 s	2.5 s			0 s	0 s	14 s	11 s	8000 s	3.4 s	3.2 s	3.3 s							.97 s		35000 s	55 s		860 s	2400 s		1400 s
MemSafety-Heap 181 tasks, max. score: 272		-350			190	0			0	0	140	-185	-41	-103	-31	-4	37						216		204	202		96	69		84
CPU time		350 s			1400 s	0 s			0 s	0 s	890 s	6800 s	3500 s	2400 s	6100 s	4500 s	66 s						1600 s		26000 s	150 s		4800 s	2700 s		5700 s
MemSafety-LinkedLists 52 tasks, max. score: 79		-246			31	0			0	0	-29	15	1	-31	4	15	48						63		-121	32		11	10		8
CPU time		27 s			530 s	0 s			0 s	0 s	130 s	68 s	39 s	1500 s	2800 s	3.6 s	1300 s						45 s		15000 s	32 s		1000 s	2300 s		1000 s
MemSafety-Other 26 tasks, max. score: 49		48			20	0			0	0	20	20	-7	3	21	47							36		48	20		46	46		46
CPU time		57 s			31 s	0 s			0 s	0 s	580 s	1700 s	370 s	640 s	660 s	330 s							1300 s		1700 s	41 s		150 s	200 s		150 s
ConcurrencySafety 1047 tasks, max. score: 1293		0			1135		1251	794		0	1020	548	601	552	756	654			1226	1293	1293	1179		-102	1208	0	389	0	0	1177	0		1293
CPU time		0 s			1800 s		14000 s	15000 s		0 s	42000 s	100000 s	160000 s	74000 s	87000 s	87000 s			5900 s	7500 s	11000 s	2000 s		90 s	77000 s	0 s	13000 s	0 s	0 s	32000 s	0 s		1300 s
ConcurrencySafety-Main 1047 tasks, max. score: 1293		0			1135	0	1251	794	0	0	1020	548	601	552	756	654			1226	1293	1293	1179		-102	1208	0	389	0	0	1177	0		1293
CPU time		0 s			1800 s	0 s	14000 s	15000 s	0 s	0 s	42000 s	100000 s	160000 s	74000 s	87000 s	87000 s			5900 s	7500 s	11000 s	2000 s		90 s	77000 s	0 s	13000 s	0 s	0 s	32000 s	0 s		1300 s
Overflows 328 tasks, max. score: 533		310			230	12				101	101	85	105	106	187	304									417	281		372	356		365
CPU time		48 s			210 s	1.1 s				1300 s	1300 s	240 s	13000 s	25 s	110 s	340 s									63000 s	340 s		3000 s	2300 s		3100 s
Overflows-BitVectors 274 tasks, max. score: 393		284			186	20			0	21	21	102	69	142	176	279									311	195		328	310		325
CPU time		44 s			46 s	1.1 s			0 s	930 s	920 s	91 s	12000 s	24 s	98 s	340 s									60000 s	63 s		2700 s	2100 s		2800 s
Overflows-Other 54 tasks, max. score: 98		46			39	0			0	29	29	8	21	7	27	45									76	54		58	56		56
CPU time		4.0 s			160 s	0 s			0 s	360 s	360 s	150 s	910 s	.67 s	13 s	4.2 s									3600 s	270 s		230 s	230 s		220 s
Termination 1437 tasks, max. score: 2513		624	1492							0	974	-307	0	0	0	0		835							0	0		2184	0		0
CPU time		4800 s	13000 s							0 s	49000 s	140 s	0 s	0 s	0 s	0 s		130 s							0 s	0 s		30000 s	0 s		0 s
Termination-MainControlFlow 247 tasks, max. score: 437		201	391		0	0			0	0	285	0	0	0	0	0		345							0	0		398	0		0
CPU time		23 s	2300 s		0 s	0 s			0 s	0 s	4000 s	0 s	0 s	0 s	0 s	0 s		60 s							0 s	0 s		2600 s	0 s		0 s
Termination-MainHeap 262 tasks, max. score: 506		-96	328		0	0			0	0	-20	-168	0	0	0	0		61							0	0		413	0		0
CPU time		120 s	7300 s		0 s	0 s			0 s	0 s	330 s	140 s	0 s	0 s	0 s	0 s		60 s							0 s	0 s		5500 s	0 s		0 s
Termination-Other 928 tasks, max. score: 1434		794	259		0	0			0	0	888	0	0	0	0	0		106							0	0		1274	0		0
CPU time		4600 s	3500 s		0 s	0 s			0 s	0 s	45000 s	0 s	0 s	0 s	0 s	0 s		11 s							0 s	0 s		22000 s	0 s		0 s
SoftwareSystems 2871 tasks, max. score: 5520		720		866	37	352			975	778	1011	254	301	-17	0	334									1695	-7079		1055	410		1067
CPU time		6300 s		6600 s	210 s	1500 s			12000 s	18000 s	55000 s	21000 s	58000 s	29 s	43 s	2400 s									73000 s	1700 s		70000 s	100000 s		65000 s
Systems_BusyBox_MemSafety 38 tasks, max. score: 72		0		0	1	0			0	0	0	0	0	0	0	0									6	-269		0	0		0
CPU time		0 s		0 s	9.1 s	0 s			0 s	0 s	0 s	0 s	0 s	0 s	0 s	0 s									9600 s	25 s		0 s	0 s		0 s
Systems_BusyBox_Overflows 38 tasks, max. score: 76		0		0	0	0			0	0	0	0	0	0	0	0									23	-31		2	2		2
CPU time		0 s		0 s	0 s	0 s			0 s	0 s	0 s	0 s	0 s	0 s	0 s	0 s									880 s	0 s		10 s	15 s		10 s
Systems_DeviceDriversLinux64_ReachSafety 2795 tasks, max. score: 5235		2104		2529	35	1028			2848	2271	2954	741	880	-50	-1	975									2817	1392	-58	2934	1050		2969
CPU time		6300 s		6600 s	210 s	1500 s			12000 s	18000 s	55000 s	21000 s	58000 s	29 s	43 s	2400 s									62000 s	1700 s	1900 s	70000 s	100000 s		65000 s
FalsificationOverall 7471 tasks, max. score: 2908		-4330			2554	343			-735	232	1302	976	184	1269	1482	1610									1154	-2698		982	900		918
CPU time		38000 s			29000 s	4500 s			23000 s	24000 s	80000 s	65000 s	170000 s	100000 s	120000 s	96000 s									90000 s	9500 s		41000 s	22000 s		23000 s
Overall 8908 tasks, max. score: 14553		-1204			4766	1972				1963	5296	1894	1674	1261	3209	4335									6917	42		7099	3837		4511
CPU time		93000 s			36000 s	22000 s				82000 s	290000 s	220000 s	340000 s	100000 s	140000 s	120000 s									660000 s	12000 s		210000 s	180000 s		120000 s
Verifiers	Plots	2LS	AProVE	BLAST	CBMC	Ceagle	CIVL	ConSequence	CPA-BAM-BnB	CPA-kInd	CPA-Seq	DepthK	ESBMC	ESBMC-falsi	ESBMC-incr	ESBMC-kind	Forester	HipTNT+	Lazy-CSeq	Lazy-CSeq-Abs	Lazy-CSeq-Swarm	MU-CSeq	PredatorHP	Skink	SMACK	Symbiotic	SymDIVINE	UAutomizer	UKojak	UL-CSeq	UTaipan	VeriAbs	Yogar-CBMC

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.

If you did not find what you are looking for, please do not hesitate to contact me (Dirk Beyer, Competition Chair).