TACAS 2021
10th Competition on Software Verification (SV-COMP 2021)

Results of the Competition

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

• Competition Report of SV-COMP 2021
• 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 2021 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. CPAchecker 3. PeSCo	MemSafety 1. Symbiotic 2. CPAchecker 3. UAutomizer	ConcurrencySafety 1. Lazy-CSeq 2. CPAchecker 3. UAutomizer
NoOverflows 1. CPAchecker 2. UAutomizer 3. UTaipan	Termination 1. UAutomizer 2. CPAchecker 3. 2LS	SoftwareSystems 1. Symbiotic 2. SMACK 3. PeSCo
FalsificationOverall 1. CPAchecker 2. PeSCo 3. UAutomizer	Overall 1. CPAchecker 2. PeSCo 3. UAutomizer
JavaOverall 1. Java-Ranger 2. JDart 3. JBMC

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 'Hors Concours' in the row for 'Representing Jury Member' means that the tool was added at the organizer's disposition and does not participate in the rankings or prize allocation.
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	CPALockator	CPAchecker	Dartagnan	DIVINE	ESBMC-incr	ESBMC-kind	Frama-C	Gazer-Theta	Goblint	Korn	Lazy-CSeq	PeSCo	Pinaka	PredatorHP	SMACK	Symbiotic	UAutomizer	UKojak	UTaipan	VeriAbs	COASTAL	Java-Ranger	JayHorn	JBMC	JDart	SPF
Representing Jury Member		Viktor Malík	Lei Bu	Michael Tautschnig	Vadim Mutilin	Pavel Andrianov	Stephan Holzner	Hernán Ponce de León	Henrich Lauko	Felipe R. Monteiro	Lucas Cordeiro	Martin Spiessl	Ákos Hajdu	Simmo Saan	Gidon Ernst	Omar Inverso	Cedric Richter	Saurabh Joshi	Hors Concours	Zvonimir Rakamaric	Marek Chalupa	Matthias Heizmann	Dominik Klumpp	Daniel Dietsch	Priyanka Darke	Hors Concours	Soha Hussein	Hossein Hojjat	Peter Schrammel	Falk Howar	Hors Concours
Affiliation		TU Brno, Czechia	Nanjing University, China	Queen Mary University of London, UK	ISP RAS, Russia	ISP RAS, Russia	LMU Munich, Germany	University of the Bundeswehr Munich, Germany	Masaryk University Brno, Czechia	Amazon Web Services, USA	University of Manchester, UK	LMU Munich, Germany	Budapest University of Technology and Economics, Hungary	University of Tartu, Estonia	LMU Munich, Germany	Gran Sasso Science Institute, Italy	Paderborn University, Germany	IIT Hyderabad, India	--	University of Utah, USA	Masaryk University Brno, Czechia	University of Freiburg, Germany	University of Freiburg, Germany	University of Freiburg, Germany	Tata Consultancy Services, India	--	University of Minnesota, USA	University of Tehran, Iran	University of Sussex and Diffblue, UK	TU Dortmund, Germany	--
ReachSafety 4927 tasks, max. score: 7844		3021		3395			4764		2012		4486			777			4526	3408			3864	3502	1768	2743	5771
CPU time		85000 s		64000 s			380000 s		120000 s		130000 s			1500 s			190000 s	22000 s			50000 s	160000 s	90000 s	140000 s	480000 s
unreach-call.ReachSafety-Arrays 436 tasks, max. score: 759		-28		-80			78	36	41		150			40			81	125			216	89	82	89	705
CPU time		100 s		5300 s			11000 s	1700 s	1900 s		1100 s			5.2 s			4100 s	2000 s			2900 s	1900 s	1500 s	4000 s	12000 s
unreach-call.ReachSafety-BitVectors 49 tasks, max. score: 83		53		43			71	2	44		57		63	8			57	40			45	48	24	47	74
CPU time		47 s		380 s			4300 s	93 s	700 s		340 s		370 s	0.29 s			2700 s	65 s			150 s	2000 s	210 s	2500 s	2900 s
unreach-call.ReachSafety-ControlFlow 92 tasks, max. score: 142		66		67			127		-80		88		59	0	71		137	33			60	92	40	73	103
CPU time		2200 s		560 s			10000 s		1200 s		3700 s		32 s	0 s	5200 s		6000 s	350 s			550 s	3700 s	2800 s	3700 s	12000 s
unreach-call.ReachSafety-ECA 1265 tasks, max. score: 2050		600		171			916		144		1096		392	2			1019	261			121	596	434	331	1268
CPU time		57000 s		32000 s			130000 s		50000 s		83000 s		27000 s	51 s			95000 s	6300 s			5100 s	43000 s	48000 s	33000 s	200000 s
unreach-call.ReachSafety-Floats 469 tasks, max. score: 893		633	0	801			747		258		780		337	2			767	801			654	645	2	646	817
CPU time		1900 s	0 s	8500 s			11000 s		8000 s		5400 s		290 s	0.095 s			14000 s	2300 s			1300 s	38000 s	13 s	37000 s	18000 s
unreach-call.ReachSafety-Heap 241 tasks, max. score: 408		139		288			282		201		254			120			284	229			309	252	220	211	295
CPU time		180 s		95 s			4500 s		810 s		400 s			69 s			5100 s	12 s			340 s	5800 s	4900 s	6800 s	9400 s
unreach-call.ReachSafety-Loops 768 tasks, max. score: 1303		383		581			635	341	675		647		628	76	646		440	709			448	615	354	-127	1015
CPU time		6900 s		10000 s			18000 s	5900 s	18000 s		19000 s		8500 s	840 s	9600 s		15000 s	5100 s			2300 s	26000 s	15000 s	23000 s	54000 s
unreach-call.ReachSafety-ProductLines 597 tasks, max. score: 929		747		298			905		792		783		865	320			849	131			323	612	329	602	860
CPU time		10000 s		570 s			80000 s		16000 s		610 s		22000 s	550 s			12000 s	18 s			1100 s	17000 s	7300 s	17000 s	96000 s
unreach-call.ReachSafety-Recursive 105 tasks, max. score: 162		0		101			61		110		110		102	52	143		61	95			111	124	85	89	125
CPU time		0 s		190 s			770 s		1100 s		890 s		350 s	5.8 s	800 s		1400 s	61 s			160 s	3200 s	1800 s	5200 s	6800 s
unreach-call.ReachSafety-Sequentialized 576 tasks, max. score: 762		132		156			462		-28		56			2			435	234			319	35	30	61	277
CPU time		4800 s		3900 s			98000 s		20000 s		1500 s			0.38 s			28000 s	2400 s			6700 s	11000 s	8100 s	4500 s	46000 s
unreach-call.ReachSafety-XCSP 119 tasks, max. score: 179		148		157			153		9		158		147	0	92		147	147			144	43	7	49	108
CPU time		2100 s		1200 s			3800 s		1800 s		2300 s		450 s	0 s	750 s		7500 s	1900 s			11000 s	6000 s	320 s	7200 s	3000 s
unreach-call.ReachSafety-Combinations 210 tasks, max. score: 270		0		0			20		0		53		0	0			0	60			132	5	0	0	105
CPU time		0 s		0 s			920 s		0 s		7400 s		0 s	0 s			0 s	1400 s			18000 s	3900 s	0 s	0 s	22000 s
MemSafety 3296 tasks, max. score: 4981		1100		-725			2992		95		1281								2187		3125	1615	925	1436
CPU time		350 s		5400 s			28000 s		180 s		24000 s								3500 s		5900 s	15000 s	8600 s	8800 s
valid-memsafety.MemSafety-Arrays 85 tasks, max. score: 145		9		27			5		0		0						5		23		45	62	38	54
CPU time		62 s		1200 s			26 s		0 s		0 s						26 s		60 s		360 s	4500 s	1800 s	2200 s
valid-memsafety.MemSafety-Heap 184 tasks, max. score: 275		70		151			179		-58		6						179		215		231	84	69	58
CPU time		14 s		1400 s			1100 s		110 s		1500 s						1100 s		2900 s		2300 s	4700 s	3000 s	2800 s
valid-memsafety.MemSafety-LinkedLists 103 tasks, max. score: 178		23		116			114		84		100						114		140		160	10	3	7
CPU time		210 s		92 s			790 s		59 s		300 s						820 s		66 s		1200 s	2000 s	53 s	1700 s
valid-memsafety.MemSafety-Other 55 tasks, max. score: 87		55		-1			52		-18		30						52		49		81	63	19	65
CPU time		14 s		66 s			410 s		9.8 s		3.4 s						420 s		500 s		2000 s	2200 s	1600 s	1400 s
valid-memcleanup.MemSafety-MemCleanup 41 tasks, max. score: 43		12		-188			35		0		0						35		12		36	21	20	17
CPU time		54 s		1.3 s			260 s		0 s		0 s						260 s		2.7 s		32 s	1400 s	2100 s	580 s
valid-memsafety.MemSafety-Juliet 2828 tasks, max. score: 4266		0		2880			4266		0		2216						4266		0		0	0	0	0
CPU time		0 s		2600 s			25000 s		0 s		22000 s						26000 s		0 s		0 s	0 s	0 s	0 s
ConcurrencySafety 1130 tasks, max. score: 1413		0		486		-819	1050	309	391	-134	37			46		1206					0	943	0	937
CPU time		0 s		2000 s		260 s	57000 s	7700 s	35000 s	9500 s	42000 s			13 s		14000 s					0 s	35000 s	0 s	34000 s
unreach-call.ConcurrencySafety-Main 1130 tasks, max. score: 1413		0		486		-819	1050	309	391	-134	37			46		1206	1050				0	943	0	937
CPU time		0 s		2000 s		260 s	57000 s	7700 s	35000 s	9500 s	42000 s			13 s		14000 s	66000 s				0 s	35000 s	0 s	34000 s
NoOverflows 452 tasks, max. score: 682		414		279			531		0		317	172		156				-200			373	512	441	506
CPU time		260 s		240 s			4400 s		0 s		530 s	28 s		7.3 s				110 s			2400 s	6100 s	5400 s	7000 s
no-overflow.NoOverflows-BitVectors 280 tasks, max. score: 402		275		186			319		0		189	115		118			319	32			202	338	293	334
CPU time		130 s		71 s			2100 s		0 s		150 s	19 s		5.0 s			2200 s	11 s			360 s	4000 s	3700 s	4300 s
no-overflow.NoOverflows-Other 172 tasks, max. score: 272		146		98			208		0		125	60		46			208	-172			160	182	156	180
CPU time		130 s		170 s			2200 s		0 s		380 s	9.7 s		2.4 s			2200 s	98 s			2100 s	2100 s	1700 s	2700 s
Termination 2212 tasks, max. score: 3897		1315		872			1356		0		832							669			1043	3019	0	0
CPU time		9000 s		5800 s			61000 s		0 s		3300 s							1200 s			13000 s	80000 s	0 s	0 s
termination.Termination-MainControlFlow 250 tasks, max. score: 443		272		60			260		0		60						260	54			-27	379	0	0
CPU time		62 s		46 s			3100 s		0 s		260 s						3100 s	10 s			81 s	3700 s	0 s	0 s
termination.Termination-MainHeap 259 tasks, max. score: 501		-26		26			0		0		24						0	56			122	385	0	0
CPU time		5.4 s		330 s			0 s		0 s		630 s						0 s	160 s			87 s	6300 s	0 s	0 s
termination.Termination-Other 1703 tasks, max. score: 2689		1356		1434			1361		0		1356						1361	808			1791	1859	0	0
CPU time		8900 s		5400 s			58000 s		0 s		2400 s						58000 s	990 s			13000 s	70000 s	0 s	0 s
SoftwareSystems 3184 tasks, max. score: 5608		-7		565	491		736		124		694			331			878			894	2001	359	298	282
CPU time		260 s		16000 s	76000 s		160000 s		9000 s		20000 s			13000 s			98000 s			52000 s	2000 s	60000 s	62000 s	74000 s
unreach-call.SoftwareSystems-AWS-C-Common-ReachSafety 175 tasks, max. score: 345		-26		88	-2		45		10		208			30			121			273	138	12	0	0
CPU time		48 s		140 s	460 s		3100 s		270 s		2200 s			37 s			5200 s			15000 s	840 s	1700 s	0 s	0 s
valid-memsafety.SoftwareSystems-BusyBox-MemSafety 37 tasks, max. score: 67		0		1	0		0		0		0						0			1	5	0	0	0
CPU time		0 s		12 s	0 s		0 s		0 s		0 s						0 s			71 s	65 s	0 s	0 s	0 s
no-overflow.SoftwareSystems-BusyBox-NoOverflows 65 tasks, max. score: 96		0		0	0		2		0		0	0		0			2			0	0	2	2	0
CPU time		0 s		0 s	0 s		480 s		0 s		0 s	0 s		0 s			480 s			0 s	0 s	34 s	57 s	0 s
unreach-call.SoftwareSystems-DeviceDriversLinux64-ReachSafety 2503 tasks, max. score: 4667		322		167	3000		2744		733		1932			1912			2664			2356	1348	2292	2033	1994
CPU time		220 s		16000 s	75000 s		160000 s		8700 s		17000 s			13000 s			92000 s			37000 s	530 s	58000 s	62000 s	74000 s
unreach-call.SoftwareSystems-DeviceDriversLinux64Large-ReachSafety 10 tasks, max. score: 20		0		0	2		0		0		0			0			0			0	0	0	0	0
CPU time		0 s		0 s	540 s		0 s		0 s		0 s			0 s			0 s			0 s	0 s	0 s	0 s	0 s
valid-memsafety.SoftwareSystems-OpenBSD-MemSafety 4 tasks, max. score: 5		0		4	0		0		0		0						0			0	2	0	0	0
CPU time		0 s		4.9 s	0 s		0 s		0 s		0 s						0 s			0 s	17 s	0 s	0 s	0 s
valid-memsafety.SoftwareSystems-uthash-MemSafety 138 tasks, max. score: 204		0		0	0		96		0		0						96			0	180	0	0	0
CPU time		0 s		0 s	0 s		710 s		0 s		0 s						710 s			0 s	400 s	0 s	0 s	0 s
no-overflow.SoftwareSystems-uthash-NoOverflows 114 tasks, max. score: 228		0		0	0		0		0		0	84		0			0			0	84	0	0	0
CPU time		0 s		0 s	0 s		0 s		0 s		0 s	12 s		0 s			0 s			0 s	40 s	0 s	0 s	0 s
unreach-call.SoftwareSystems-uthash-ReachSafety 138 tasks, max. score: 276		0		0	0		0		0		0			0			0			0	228	0	0	0
CPU time		0 s		0 s	0 s		0 s		0 s		0 s			0 s			0 s			0 s	95 s	0 s	0 s	0 s
FalsificationOverall 12989 tasks, max. score: 6173		1436		2609			4356		306		2002						4329				2947	3432	1800	3336
CPU time		28000 s		43000 s			250000 s		110000 s		100000 s						170000 s				45000 s	110000 s	33000 s	76000 s
Overall 15201 tasks, max. score: 23778		6219		5289			12217		2083		6656						12208				9268	11769	4332	7676
CPU time		95000 s		93000 s			690000 s		160000 s		220000 s						450000 s				74000 s	360000 s	170000 s	270000 s
JavaOverall 473 tasks, max. score: 693																										298	630	369	603	623	409
CPU time																										2900 s	18000 s	25000 s	780 s	3400 s	2100 s
assert_java.ReachSafety-Java 473 tasks, max. score: 693																										298	630	369	603	623	409
CPU time																										2900 s	18000 s	25000 s	780 s	3400 s	2100 s
Participants	Plots	2LS	BRICK	CBMC	CPA-BAM-BnB	CPALockator	CPAchecker	Dartagnan	DIVINE	ESBMC-incr	ESBMC-kind	Frama-C	Gazer-Theta	Goblint	Korn	Lazy-CSeq	PeSCo	Pinaka	PredatorHP	SMACK	Symbiotic	UAutomizer	UKojak	UTaipan	VeriAbs	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).