TACAS 2018
7th Competition on Software Verification (SV-COMP)

Results of the Competition

This web page presents the results of the 2018 7th International Competition on Software Verification (SV-COMP '18).

• 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. CPA-Seq 2. VeriAbs 3. UAutomizer	MemSafety 1. Symbiotic 2. PredatorHP 3. UKojak	ConcurrencySafety 1. Yogar-CBMC 2. CPA-Seq 3. CBMC
NoOverflows 1. UAutomizer 2. CPA-Seq 3. UTaipan	Termination 1. UAutomizer 2. AProVE 3. CPA-Seq	SoftwareSystems 1. CPA-BAM-BnB 2. UAutomizer 3. CPA-BAM-Slicing
FalsificationOverall 1. CPA-Seq 2. CBMC 3. Symbiotic	Overall 1. CPA-Seq 2. UAutomizer 3. ESBMC-kind

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	CBMC	CPA-BAM-BnB	CPA-BAM-Slicing	CPA-Seq	DepthK	ESBMC-incr	ESBMC-kind	Forester	InterpChecker	Map2Check	PredatorHP	Skink	Symbiotic	UAutomizer	UKojak	UTaipan	VeriAbs	VIAP	Yogar-CBMC
Representing Jury Member		Peter Schrammel	Jera Hensel	Michael Tautschnig	Vadim Mutilin	Mikhail Mandrykin	Thomas Lemberger	Hussama Ismail	Felipe Monteiro	Mikhail R. Gadelha	Martin Hruska	Zhao Duan	Herbert Oliveira Rocha	Veronika Šoková	Franck Cassez	Marek Chalupa	Matthias Heizmann	Alexander Nutz	Daniel Dietsch	Priyanka Darke	Pritom Rajkhowa	Liangze Yin
Affiliation		University of Sussex, UK	RWTH Aachen University, Germany	Queen Mary University of London, UK	ISP RAS, Moscow, Russia	ISP RAS, Moscow, Russia	LMU Munich, Germany	Federal University of Amazonas, Brazil	Federal University of Amazonas, Brazil	University of Southampton, UK	BUT, Brno, Czech Republic	Xidian University, China	Federal University of Roraima, Brazil	BUT, Brno, Czech Republic	Macquarie University, Australia	Masaryk University, Brno, Czech Republic	University of Freiburg, Germany	University of Freiburg, Germany	University of Freiburg, Germany	Tata Consultancy Services, India	Hong Kong University of Science and Technology, China	National University of Defense Technology, China
ReachSafety 2941 tasks, max. score: 4775		2016		2117			3058	1594	2106	2363		-8183				2227	2475	1619	1969	2760
CPU time		79000 s		33000 s			180000 s	150000 s	44000 s	47000 s		87000 s				21000 s	110000 s	58000 s	71000 s	170000 s
ReachSafety-Arrays 167 tasks, max. score: 290		-55		26	-297	-758	16	3	34	38		-545	34		52	146	16	15	18	235	209
CPU time		600 s		1000 s	47 s	340 s	1700 s	1300 s	570 s	580 s		2400 s	1700 s		480 s	350 s	390 s	380 s	150 s	10000 s	7000 s
ReachSafety-BitVectors 50 tasks, max. score: 86		56		49	-155	-149	77	53	56	56		-508	-68		36	54	58	33	56	53
CPU time		98 s		560 s	170 s	320 s	1600 s	3900 s	330 s	350 s		710 s	880 s		180 s	1400 s	1800 s	1600 s	3200 s	1100 s
ReachSafety-ControlFlow 94 tasks, max. score: 146		63		59	-190	104	108	61	45	70		-51			22	62	97	44	46	51
CPU time		150 s		310 s	920 s	1200 s	1900 s	1800 s	150 s	180 s		3300 s			46 s	13 s	4500 s	2500 s	8000 s	3700 s
ReachSafety-ECA 1148 tasks, max. score: 1886		724		142	770	492	1179	89	305	303		365				75	792	345	184	918
CPU time		64000 s		25000 s	80000 s	15000 s	120000 s	40000 s	35000 s	37000 s		58000 s				6800 s	76000 s	39000 s	24000 s	82000 s
ReachSafety-Floats 172 tasks, max. score: 313		251		259	-714	-235	181	54	257	263		-1424			91	83	131	93	131	202
CPU time		4800 s		3100 s	310 s	420 s	6000 s	2800 s	5100 s	5500 s		560 s			370 s	18 s	4100 s	610 s	4200 s	9200 s
ReachSafety-Heap 181 tasks, max. score: 291		108		192	-168	71	193	163	174	191	139	113	46	203	135	201	200	186	157	129
CPU time		13 s		170 s	500 s	780 s	4200 s	1000 s	41 s	44 s	1300 s	1200 s	75 s	81 s	510 s	24 s	2200 s	3200 s	3300 s	1700 s
ReachSafety-Loops 163 tasks, max. score: 274		139		106	137	59	178	119	91	134		13	-134		154	152	189	159	191	216	44
CPU time		690 s		570 s	1700 s	1700 s	4900 s	3400 s	2000 s	1900 s		1800 s	1200 s		860 s	520 s	2300 s	2400 s	2900 s	6500 s	210 s
ReachSafety-ProductLines 597 tasks, max. score: 929		795		301	711	663	919	443	453	573		203				461	626	440	529	513
CPU time		7800 s		660 s	20000 s	4100 s	7000 s	69000 s	710 s	1100 s		9900 s				200 s	7700 s	4300 s	19000 s	31000 s
ReachSafety-Recursive 96 tasks, max. score: 148		0		95	-630	-640	108	42	99	99		-636	98		51	103	116	61	104	81	91
CPU time		0 s		460 s	160 s	120 s	490 s	560 s	380 s	420 s		130 s	290 s		400 s	12 s	1800 s	840 s	5000 s	4900 s	650 s
ReachSafety-Sequentialized 273 tasks, max. score: 376		143		164	-364	10	194	134	79	77		-86				143	42	19	13	180
CPU time		1700 s		1600 s	2600 s	2000 s	26000 s	22000 s	480 s	490 s		9500 s				12000 s	5700 s	3000 s	1400 s	22000 s
MemSafety 326 tasks, max. score: 539		169		132			181	-28	115	238	83		228	286		411	254	265	249
CPU time		130 s		1800 s			1700 s	3400 s	1400 s	1300 s	1300 s		4000 s	2100 s		310 s	5200 s	11000 s	3200 s
MemSafety-Arrays 69 tasks, max. score: 117		1		2	0	0	6	13	14	15			106	7		105	42	70	53
CPU time		.24 s		8.0 s	0 s	0 s	15 s	6.7 s	3.4 s	3.8 s			2300 s	.96 s		23 s	240 s	3100 s	600 s
MemSafety-Heap 180 tasks, max. score: 270		46		123	0	0	183	-234	113	129	35		174	201		199	87	69	78
CPU time		120 s		1600 s	0 s	0 s	650 s	2800 s	1400 s	1300 s	67 s		1400 s	1600 s		71 s	3000 s	5900 s	2100 s
MemSafety-LinkedLists 51 tasks, max. score: 78		2		11	0	0	16	4	-6	11	42		11	50		27	13	4	4
CPU time		.77 s		200 s	0 s	0 s	77 s	3.2 s	3.7 s	4.0 s	1300 s		14 s	39 s		57 s	1800 s	1500 s	360 s
MemSafety-Other 26 tasks, max. score: 49		46		18	0	0	21	18	18	46			2	34		49	46	46	46
CPU time		7.3 s		9.1 s	0 s	0 s	920 s	600 s	2.6 s	4.4 s			310 s	400 s		150 s	120 s	180 s	120 s
ConcurrencySafety 1047 tasks, max. score: 1293		0		765			969	10	345	333						0	0	0	0			1266
CPU time		0 s		1300 s			42000 s	59000 s	67000 s	67000 s						0 s	0 s	0 s	0 s			1100 s
ConcurrencySafety-Main 1047 tasks, max. score: 1293		0		765	0	-24038	969	10	345	333						0	0	0	0			1266
CPU time		0 s		1300 s	0 s	860 s	42000 s	59000 s	67000 s	67000 s						0 s	0 s	0 s	0 s			1100 s
NoOverflows 358 tasks, max. score: 574		281		214			436	-101	221	328			-263			324	447	408	427
CPU time		91 s		100 s			2000 s	150 s	92 s	89 s			220 s			98 s	2500 s	2400 s	2200 s
NoOverflows-BitVectors 280 tasks, max. score: 402		274		188	0	0	313	-32	188	297			88			195	351	318	319
CPU time		87 s		88 s	0 s	0 s	1200 s	0 s	64 s	81 s			94 s			42 s	2200 s	2100 s	1900 s
NoOverflows-Other 78 tasks, max. score: 138		46		41	0	0	103	-35	44	60			-139			87	97	89	97
CPU time		4.1 s		16 s	0 s	0 s	840 s	150 s	28 s	8.2 s			120 s			56 s	310 s	290 s	300 s
Termination 2009 tasks, max. score: 3528		1522	2317	825			1628	-274	824	824						0	3022	0	0
CPU time		9800 s	64000 s	4400 s			58000 s	290 s	3000 s	3000 s						0 s	37000 s	0 s	0 s
Termination-MainControlFlow 250 tasks, max. score: 444		269	376	60	0	0	291	0	60	60						0	397	0	0
CPU time		73 s	2000 s	66 s	0 s	0 s	2400 s	0 s	270 s	260 s						0 s	2400 s	0 s	0 s
Termination-MainHeap 260 tasks, max. score: 503		100	336	24	0	0	67	-136	24	24						0	409	0	0
CPU time		31 s	6800 s	66 s	0 s	0 s	6900 s	140 s	610 s	610 s						0 s	4600 s	0 s	0 s
Termination-Other 1499 tasks, max. score: 2336		1218	995	1348	0	0	1513	170	1346	1346						0	2025	0	0
CPU time		9700 s	55000 s	4300 s	0 s	0 s	48000 s	160 s	2200 s	2200 s						0 s	30000 s	0 s	0 s
SoftwareSystems 2842 tasks, max. score: 5014		102		-11	1270	1050	1018	255	-24	779		753				571	1163	727	1050
CPU time		26 s		290 s	39000 s	10000 s	68000 s	20000 s	1100 s	12000 s		18000 s				2000 s	110000 s	160000 s	110000 s
Systems_BusyBox_MemSafety 38 tasks, max. score: 72		0		0	0	0	0	0	1	1		0				1	0	0	0
CPU time		0 s		0 s	0 s	0 s	0 s	0 s	780 s	400 s		0 s				2.0 s	0 s	0 s	0 s
Systems_BusyBox_NoOverflows 70 tasks, max. score: 107		0		0	0	0	0	0	0	0		0				0	4	4	4
CPU time		0 s		0 s	0 s	0 s	0 s	0 s	0 s	0 s		0 s				0 s	23 s	47 s	23 s
Systems_DeviceDriversLinux64_ReachSafety 2734 tasks, max. score: 5112		295		-31	3665	3030	2937	735	-142	2176		2172				1575	3200	1941	2873
CPU time		26 s		290 s	39000 s	10000 s	68000 s	20000 s	320 s	12000 s		18000 s				2000 s	110000 s	160000 s	110000 s
FalsificationOverall 7514 tasks, max. score: 3189		678		1611			2213	-831	1146	1307						1461	1000	892	872
CPU time		41000 s		29000 s			100000 s	80000 s	64000 s	67000 s						21000 s	45000 s	22000 s	27000 s
Overall 9523 tasks, max. score: 15291		4417		4541			7792	219	3835	5476						4959	7590	4374	4750
CPU time		89000 s		41000 s			350000 s	230000 s	120000 s	130000 s						23000 s	260000 s	230000 s	190000 s
Verifiers	Plots	2LS	AProVE	CBMC	CPA-BAM-BnB	CPA-BAM-Slicing	CPA-Seq	DepthK	ESBMC-incr	ESBMC-kind	Forester	InterpChecker	Map2Check	PredatorHP	Skink	Symbiotic	UAutomizer	UKojak	UTaipan	VeriAbs	VIAP	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 Web Master).