TACAS 2020
9th Competition on Software Verification (SV-COMP 2020)

Results of the Competition

This web page presents the results of SV-COMP 2020 - 9th International Competition on Software Verification.

• Competition Report of SV-COMP 2020
• The benchmarks and rules are also available from the competition web site.
• Statistics on validation results are also available.

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 about what you can learn from a score-based quantile plot and how to interpret it, is described in the SV-COMP 2015 report, on pages 12 and 13.

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 SV-COMP 2020 results archive, which contains all 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)

ReachSafety 1. VeriAbs 2. CPA-Seq 3. PeSCo	MemSafety 1. PredatorHP 2. Symbiotic 3. CPA-Seq	ConcurrencySafety 1. Lazy-CSeq 2. Yogar-CBMC 3. CPA-Seq
NoOverflows 1. CPA-Seq 2. UAutomizer 3. UTaipan	Termination 1. UAutomizer 2. CPA-Seq 3. 2LS	SoftwareSystems 1. Symbiotic 2. CPA-Seq 3. CPA-BAM-BnB
FalsificationOverall 1. CPA-Seq 2. Symbiotic 3. ESBMC	Overall 1. CPA-Seq 2. UAutomizer 3. PeSCo
JavaOverall 1. Java-Ranger 2. JBMC 3. JDart

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

Participants	Plots	2LS	BRICK	CBMC	CPA-BAM-BnB	CPA-Seq	CPALockator	Dartagnan	DIVINE	ESBMC	GACAL	Lazy-CSeq	Map2Check	PeSCo	Pinaka	PredatorHP	Symbiotic	UAutomizer	UKojak	UTaipan	VeriAbs	VeriFuzz	Yogar-CBMC	COASTAL	Java-Ranger	JayHorn	JBMC	JDart	SPF
Representing Jury Member		Viktor Malík	Lei Bu	Michael Tautschnig	Vadim Mutilin	Martin Spiessl	Pavel Andrianov	Hernan Ponce de Leon	Henrich Lauko	Felipe R. Monteiro	Benjamin Quiring	Omar Inverso	Herbert Rocha	Cedric Richter	Saurabh Joshi	Veronika Šoková	Marek Chalupa	Matthias Heizmann	Alexander Nutz	Daniel Dietsch	Priyanka Darke	Raveendra Kumar Medicherla	Liangze Yin	Willem Visser	Vaibhav Sharma	Philipp Ruemmer	Peter Schrammel	Falk Howar	Willem Visser
Affiliation		Brno University of Technology, Czechia	Nanjing University, China	Amazon Web Services, UK	ISP RAS, Russia	LMU Munich, Germany	ISP RAS, Russia	fortiss GmbH, Germany	Masaryk University, Czechia	Federal University of Amazonas, Brazil	Northeastern University, USA	Gran Sasso Science Institute, Italy	Federal University of Roraima, Brazil	Paderborn University, Germany	IIT Hyderabad, India	Brno University of Technology, Czechia	Masaryk University, Czechia	University of Freiburg, Germany	University of Freiburg, Germany	University of Freiburg, Germany	Tata Consultancy Services, India	Tata Consultancy Services, India	National University of Defense Technology, China	Stellenbosch University, South Africa	University of Minnesota, USA	Uppsala University, Sweden	University of Sussex, UK	TU Dortmund, Germany	Amazon, USA
ReachSafety 4079 tasks, max. score: 6681		2491		2864		4396			-76	3481				4376	2585		2753	2696	1702	2185	5543	1206
CPU time		83000 s		42000 s		260000 s			77000 s	99000 s				140000 s	17000 s		110000 s	170000 s	92000 s	86000 s	530000 s	91000 s
ReachSafety-Arrays 436 tasks, max. score: 759		-28		-65		28			48	150			379	77	129		213	82	75	85	694	105
CPU time		100 s		1300 s		2700 s			3500 s	1100 s			52000 s	1700 s	3100 s		2300 s	1500 s	1400 s	2900 s	9200 s	820 s
ReachSafety-BitVectors 47 tasks, max. score: 79		49		53		72			29	51			46	73	40		60	58	22	50	75	14
CPU time		47 s		310 s		1600 s			390 s	320 s			11000 s	1500 s	75 s		2800 s	1600 s	550 s	3600 s	4600 s	290 s
ReachSafety-ControlFlow 95 tasks, max. score: 148		66		68		141			-440	58			-385	145	33		58	97	41	85	116	20
CPU time		2000 s		320 s		6700 s			4100 s	2600 s			7800 s	4000 s	410 s		9500 s	5700 s	2900 s	4600 s	15000 s	850 s
ReachSafety-ECA 1256 tasks, max. score: 2041		600		145		1147			0	1119				905	261		321	1097	304	335	1734	430
CPU time		59000 s		25000 s		130000 s			0 s	81000 s				77000 s	7700 s		18000 s	110000 s	62000 s	18000 s	240000 s	55000 s
ReachSafety-Floats 466 tasks, max. score: 887		627	800	788		749			330	778				733	796		502	-505	2	-510	814	41
CPU time		1700 s	710 s	6300 s		12000 s			7900 s	7000 s				13000 s	2300 s		130 s	19000 s	9.9 s	19000 s	25000 s	900 s
ReachSafety-Heap 237 tasks, max. score: 402		141		273		276			225	245			194	279	224	325	233	248	207	182	297	56
CPU time		280 s		51 s		4400 s			480 s	270 s			83000 s	3300 s	14 s	150 s	130 s	4700 s	4200 s	2200 s	13000 s	350 s
ReachSafety-Loops 286 tasks, max. score: 506		158		155		198			118	98	112		-13	202	147		169	279	223	280	364	56
CPU time		1500 s		3300 s		6800 s			2400 s	4300 s	1900 s		49000 s	3800 s	630 s		4800 s	6700 s	7300 s	7400 s	19000 s	930 s
ReachSafety-ProductLines 597 tasks, max. score: 929		743		338		929			340	783				929	131		453	638	304	590	902	257
CPU time		12000 s		320 s		12000 s			45000 s	600 s				13000 s	23 s		1700 s	12000 s	5900 s	16000 s	120000 s	3300 s
ReachSafety-Recursive 104 tasks, max. score: 160		0		107		88			106	108			103	88	90		111	119	66	121	126	45
CPU time		0 s		440 s		2200 s			1200 s	940 s			24000 s	3100 s	90 s		140 s	2200 s	1000 s	6200 s	7100 s	2000 s
ReachSafety-Sequentialized 555 tasks, max. score: 727		121		128		509			33	115				496	212		-200	79	32	73	447	267
CPU time		6300 s		5200 s		84000 s			12000 s	1300 s				21000 s	2600 s		74000 s	11000 s	6800 s	6800 s	72000 s	27000 s
MemSafety 512 tasks, max. score: 809		298		-162		355			71	334			-68			611	516	354	231	316	0
CPU time		410 s		3000 s		2700 s			300 s	1900 s			45000 s			2800 s	1800 s	15000 s	13000 s	8200 s	0 s
MemSafety-Arrays 78 tasks, max. score: 133		0		27		4			1	18			32	4		21	22	67	37	53	0
CPU time		0 s		1600 s		18 s			2.2 s	3.3 s			3700 s	18 s		56 s	42 s	3200 s	1000 s	3100 s	0 s
MemSafety-Heap 179 tasks, max. score: 268		73		123		179			57	142			174	179		217	204	78	69	82	0
CPU time		19 s		1300 s		1100 s			180 s	1500 s			23000 s	1100 s		2600 s	520 s	4000 s	5500 s	2700 s	0 s
MemSafety-LinkedLists 102 tasks, max. score: 176		23		111		112			69	115			102	112		150	128	-10	-27	-26	0
CPU time		210 s		52 s		770 s			86 s	300 s			10000 s	780 s		72 s	140 s	4300 s	1900 s	200 s	0 s
MemSafety-Other 52 tasks, max. score: 81		49		-6		48			-9	18			-143	48		76	52	69	36	69	0
CPU time		28 s		40 s		590 s			36 s	75 s			2700 s	600 s		15 s	1100 s	1000 s	1800 s	1200 s	0 s
MemSafety-TerminCrafted 64 tasks, max. score: 126		97		15		11			0	91			14	11		117	93	123	115	123	0
CPU time		65 s		12 s		28 s			0 s	6.8 s			5200 s	28 s		11 s	18 s	600 s	560 s	680 s	0 s
MemSafety-MemCleanup 37 tasks, max. score: 38		15		-153		34			0	0			-24	34		34	34	-11	-14	-16	0
CPU time		84 s		1.1 s		220 s			0 s	0 s			730 s	220 s		55 s	20 s	1600 s	2200 s	400 s	0 s
ConcurrencySafety 1082 tasks, max. score: 1344		0		554		996	-387	173	550	325		1279					0	296	0	289	0		1275
CPU time		0 s		1200 s		44000 s	240 s	10000 s	12000 s	3000 s		24000 s					0 s	5900 s	0 s	5600 s	0 s		1400 s
ConcurrencySafety-Main 1082 tasks, max. score: 1344		0		554		996	-387	173	550	325		1279		952			0	296	0	289	0		1275
CPU time		0 s		1200 s		44000 s	240 s	10000 s	12000 s	3000 s		24000 s		52000 s			0 s	5900 s	0 s	5600 s	0 s		1400 s
NoOverflows 397 tasks, max. score: 612		340		268		483			0	264			-89		243		294	466	387	461	0	146
CPU time		190 s		98 s		3400 s			0 s	250 s			28000 s		90 s		3100 s	4900 s	5000 s	5400 s	0 s	2100 s
NoOverflows-BitVectors 280 tasks, max. score: 402		274		191		313			0	188			-6	313	170		202	348	290	342	0	137
CPU time		120 s		51 s		1800 s			0 s	160 s			16000 s	1800 s	20 s		190 s	3900 s	3400 s	3700 s	0 s	2000 s
NoOverflows-Other 117 tasks, max. score: 193		86		78		154			0	77			-50	154	72		89	129	107	129	0	29
CPU time		64 s		47 s		1500 s			0 s	94 s			12000 s	1500 s	70 s		2900 s	990 s	1600 s	1700 s	0 s	160 s
Termination 2043 tasks, max. score: 3563		1264		499		1720			0	777					590		1022	2942	0	0	0
CPU time		12000 s		2400 s		58000 s			0 s	5600 s					1100 s		14000 s	55000 s	0 s	0 s	0 s
Termination-MainControlFlow 249 tasks, max. score: 443		275		60		317			0	60				320	54		85	398	0	0	0
CPU time		64 s		30 s		2200 s			0 s	240 s				2800 s	11 s		130 s	3400 s	0 s	0 s	0 s
Termination-MainHeap 260 tasks, max. score: 503		-26		24		59			0	24				59	56		58	391	0	0	0
CPU time		5.4 s		24 s		3700 s			0 s	610 s				3700 s	160 s		14 s	4400 s	0 s	0 s	0 s
Termination-Other 1534 tasks, max. score: 2330		1307		612		1573			0	1240				1577	666		1437	1869	0	0	0
CPU time		12000 s		2300 s		52000 s			0 s	4800 s				54000 s	960 s		14000 s	47000 s	0 s	0 s	0 s
SoftwareSystems 2939 tasks, max. score: 4879		13		30	602	746			-12	500							954	591	501	482	244
CPU time		300 s		6300 s	29000 s	76000 s			14 s	14000 s							890 s	46000 s	65000 s	57000 s	26000 s
SoftwareSystems-AWS-C-Common-ReachSafety 123 tasks, max. score: 246		-12		11	-15	49			8	66				-294			147	6	0	0	-86
CPU time		20 s		250 s	380 s	1800 s			7.2 s	1100 s				1400 s			42 s	1200 s	0 s	0 s	71 s
SoftwareSystems-BusyBox-MemSafety 40 tasks, max. score: 76		0		0	0	0			0	0				0			0	0	0	0	0
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
SoftwareSystems-BusyBox-NoOverflows 70 tasks, max. score: 107		0		0	0	-16			0	-32				-16			0	2	2	2	0
CPU time		0 s		0 s	0 s	0 s			0 s	0 s				0 s			0 s	22 s	40 s	21 s	0 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 2705 tasks, max. score: 5062		322		-103	3100	2976			-229	2086				2287			1158	2511	2229	2142	3016
CPU time		280 s		6000 s	28000 s	75000 s			6.4 s	13000 s				170000 s			850 s	45000 s	65000 s	57000 s	26000 s
SoftwareSystems-OpenBSD-MemSafety 1 tasks, max. score: 1		0		0	0	0			0	0				0			0	0	0	0	0
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
FalsificationOverall 9009 tasks, max. score: 4211		914		1256		2772			585	1639				1590			1828	893	1148	805	273
CPU time		27000 s		30000 s		160000 s			66000 s	52000 s				110000 s			96000 s	79000 s	36000 s	33000 s	260000 s
Overall 11052 tasks, max. score: 17328		4924		3365		9219			1151	5567				8023			5985	8178	3710	5057	2656
CPU time		96000 s		55000 s		440000 s			89000 s	120000 s				430000 s			130000 s	300000 s	170000 s	160000 s	550000 s
JavaOverall 416 tasks, max. score: 602																								472	549	278	527	524	410
CPU time																								1500 s	4700 s	3800 s	630 s	950 s	1500 s
ReachSafety-Java 416 tasks, max. score: 602																								472	549	278	527	524	410
CPU time																								1500 s	4700 s	3800 s	630 s	950 s	1500 s
Participants	Plots	2LS	BRICK	CBMC	CPA-BAM-BnB	CPA-Seq	CPALockator	Dartagnan	DIVINE	ESBMC	GACAL	Lazy-CSeq	Map2Check	PeSCo	Pinaka	PredatorHP	Symbiotic	UAutomizer	UKojak	UTaipan	VeriAbs	VeriFuzz	Yogar-CBMC	COASTAL	Java-Ranger	JayHorn	JBMC	JDart	SPF

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 Dirk Beyer (competition chair).