TACAS 2023
12th Competition on Software Verification (SV-COMP 2023)

Results of the Competition

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

• Competition Report of SV-COMP 2023
• The benchmarks and rules are also available from the competition web site.
• Results of the Witness-Validation Track 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 2022 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. VeriAbsL 3. PeSCo-CPA	MemSafety 1. Symbiotic 2. CPAchecker 3. UTaipan	ConcurrencySafety 1. Deagle 2. UAutomizer 3. UGemCutter
NoOverflows 1. UAutomizer 2. UTaipan 3. UKojak	Termination 1. VeriFuzz 2. UAutomizer 3. 2LS	SoftwareSystems 1. Symbiotic 2. Bubaak 3. Mopsa
FalsificationOverall 1. Bubaak 2. PeSCo-CPA 3. CPAchecker	Overall 1. UAutomizer 2. PeSCo-CPA 3. CPAchecker
JavaOverall 1. JBMC 2. GDart 3. MLB

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	Bubaak	CBMC	CoVeriTeam-Verifier-AlgoSelection	CoVeriTeam-Verifier-ParallelPortfolio	CPA-BAM-BnB	CPA-BAM-SMG	CPALockator	CPAchecker	Crux	CSeq	Dartagnan	Deagle	DIVINE	EBF	ESBMC-incr	ESBMC-kind	Frama-C-SV	Gazer-Theta	GDart-LLVM	Goblint	Graves-CPA	Graves-Par	Infer	Korn	Lazy-CSeq	LF-checker	Locksmith	Mopsa	PeSCo-CPA	PIChecker	Pinaka	PredatorHP	Symbiotic	Theta	UAutomizer	UGemCutter	UKojak	UTaipan	VeriAbs	VeriAbsL	VeriFuzz	VeriOover	COASTAL	GDart	Java-Ranger	JayHorn	JBMC	JDart	MLB	SPF
Representing Jury Member		Viktor Malík	Lei Bu	Marek Chalupa	Michael Tautschnig	Hors Concours	Hors Concours	Hors Concours	Hors Concours	Hors Concours	Henrik Wachowitz	Hors Concours	Hors Concours	Hernán Ponce de León	Fei He	Hors Concours	Fatimah Aljaafari	Hors Concours	Rafael Sá Menezes	Martin Spiessl	Hors Concours	Falk Howar	Simmo Saan	Will Leeson	Hors Concurs	Hors Concours	Gidon Ernst	Hors Concours	Tong Wu	Vesal Vojdani	Raphaël Monat	Cedric Richter	Jie Su	Hors Concours	Hors Concours	Marek Trtik	Levente Bajczi	Matthias Heizmann	Dominik Klumpp	Frank Schüssele	Daniel Dietsch	Priyanka Darke	Priyanka Darke	Raveendra Kumar Medicherla	HaiPeng Qu	Hors Concours	Falk Howar	Soha Hussein	Hors Concours	Peter Schrammel	Hors Concours	Lei Bu	Hors Concours
Affiliation		Brno University of Technology, Czechia	Nanjing University, China	ISTA, Austria	Queen Mary University of London, UK	--, --	--, --	--, --	--, --	--, --	LMU Munich, Germany	--, --	--, --	Huawei Dresden Research Center, Germany	Tsinghua University, China	--, --	University of Manchester, UK	--, --	University of Manchester, UK	LMU Munich, Germany	--, --	TU Dortmund, Germany	University of Tartu, Estonia	University of Virginia, USA	University of Virginia, USA	--, --	LMU Munich, Germany	--, --	University of Manchester, UK	University of Tartu, Estonia	Inria and University of Lille, France	University of Oldenburg, Germany	Xidian University, China	--, --	--, --	Masaryk University, Brno, Czechia	Budapest University of Technology and Economics, Hungary	University of Freiburg, Germany	University of Freiburg, Germany	University of Freiburg, Germany	University of Freiburg, Germany	Tata Consultancy Services, India	Tata Consultancy Services, India	Tata Consultancy Services, India	Ocean University of China, China	--, --	TU Dortmund, Germany	University of Minnesota, USA	--, --	University of Sussex and Diffblue, UK	--, --	Nanjing University, China	--, --
ReachSafety 6138 tasks, max. score: 9814		3617		4278	3497	-507	2033				5535	879				2698			5183				874	4868	-64	-56129					699	5576		3387		4786	1076	3997		2306	3672	6628	6478	1704
CPU time		90000 s		130000 s	120000 s	350000 s	310000 s				530000 s	6900 s				130000 s			130000 s				220 s	170000 s	34000 s	48 s					460 s	280000 s		19000 s		100000 s	98000 s	200000 s		99000 s	160000 s	540000 s	420000 s	57000 s
ReachSafety-Arrays 300 tasks, max. score: 509		8	119	149	-74	164	165				70	-20				35			100	0			14	61	0	-3092					6	83		79		150	11	74		76	75	381	348	71
CPU time		540 s	450 s	1400 s	1700 s	9100 s	1700 s				9100 s	96 s				1000 s			1200 s	0 s			3.2 s	1700 s	0 s	3.8 s					3.1 s	2600 s		860 s		550 s	1100 s	1700 s		1900 s	2600 s	18000 s	14000 s	480 s
ReachSafety-BitVectors 49 tasks, max. score: 83		43	49	44	39	46	71				61	44				42			53	0	55	32	20	53	2	-654					8	62		40		47	28	54		24	43	69	68	15
CPU time		190 s	590 s	180 s	380 s	1500 s	5300 s				3700 s	68 s				710 s			330 s	0 s	210 s	1700 s	1.3 s	1200 s	400 s	0.29 s					4.0 s	2200 s		64 s		670 s	540 s	2200 s		410 s	2200 s	2800 s	2300 s	150 s
ReachSafety-ControlFlow 22 tasks, max. score: 37		24		6	4	2	34				26	-26				26			28		24		0	20	3	-240	31				0	32		2		19	10	25		27	27	31	33	6
CPU time		2.5 s		27 s	27 s	130 s	810 s				2800 s	6.2 s				120 s			68 s		3.8 s		0 s	1000 s	190 s	0 s	190 s				0 s	480 s		0.090 s		2400 s	870 s	680 s		990 s	410 s	1300 s	900 s	360 s
ReachSafety-ECA 1263 tasks, max. score: 2046		544		280	308	356	1057				1008	10				143			1089	0	161		0	669	0	-12732					2	1053		261		274	132	786		388	328	1226	1287	390
CPU time		68000 s		9900 s	68000 s	81000 s	97000 s				160000 s	320 s				49000 s			78000 s	0 s	7600 s		0 s	50000 s	0 s	29 s					3.4 s	130000 s		4900 s		5400 s	39000 s	85000 s		52000 s	22000 s	210000 s	170000 s	29000 s
ReachSafety-Floats 434 tasks, max. score: 824		605	798	682	754	775	780				706	573				230			750		329		44	699	607						60	711		770		681	-42	427		2	431	789	775	-6
CPU time		3000 s	2400 s	1700 s	7300 s	25000 s	9000 s				6900 s	72 s				7100 s			10000 s		280 s		2.7 s	8500 s	9500 s						32 s	12000 s		2300 s		850 s	4300 s	22000 s		19 s	22000 s	16000 s	9000 s	490 s
ReachSafety-Heap 159 tasks, max. score: 257		85		132	147	135	106				137	-134				71			99				52	138	31	-1466					62	144		92		166	2	110		111	98	166	154	59
CPU time		630 s		140 s	54 s	6800 s	660 s				2700 s	85 s				630 s			940 s				23 s	1900 s	1700 s	3.4 s					36 s	1900 s		5.1 s		98 s	23 s	3000 s		5200 s	2200 s	8900 s	4600 s	340 s
ReachSafety-Loops 685 tasks, max. score: 1159		423		586	573	520	619				666	486				637			566	0	522		130	553	12	-7508	323				168	636		596		789	473	759		458	738	836	762	198
CPU time		8300 s		14000 s	8000 s	25000 s	26000 s				21000 s	820 s				17000 s			13000 s	0 s	2000 s		20 s	15000 s	3200 s	4.0 s	1200 s				200 s	10000 s		3900 s		31000 s	42000 s	29000 s		19000 s	34000 s	47000 s	33000 s	3300 s
ReachSafety-ProductLines 597 tasks, max. score: 929		706		453	283	351	911				905	247				803			782	0	675		316	809	0						282	903		131		453	0	554		272	576	902	911	260
CPU time		1700 s		3500 s	420 s	19000 s	29000 s				79000 s	3500 s				18000 s			660 s	0 s	450 s		80 s	8100 s	0 s						150 s	15000 s		19 s		4000 s	0 s	11000 s		7000 s	23000 s	96000 s	56000 s	1700 s
ReachSafety-Recursive 59 tasks, max. score: 91		0		56	38	51	50				27	24				45			44	0	38		12	28	0	-404	79				0	29		30		56	13	58		38	57	50	46	24
CPU time		0 s		2300 s	200 s	2100 s	750 s				380 s	27 s				810 s			2300 s	0 s	180 s		1.3 s	480 s	0 s	1.8 s	400 s				0 s	980 s		130 s		2100 s	370 s	2500 s		860 s	1900 s	2100 s	4300 s	440 s
ReachSafety-Sequentialized 563 tasks, max. score: 736		12		338	75	385	456				489	1				-25			144				2	378	0	-2656					2	459		229		332	13	40		40	-45	463	519	91
CPU time		2100 s		25000 s	2600 s	85000 s	60000 s				110000 s	810 s				21000 s			610 s				0.94 s	14000 s	0 s	0 s					0.98 s	44000 s		2300 s		10000 s	2000 s	7700 s		9800 s	5900 s	58000 s	63000 s	5400 s
ReachSafety-XCSP 114 tasks, max. score: 174		143		136	152	151	149				146	96				4			150		145		0	147	0	-960	92				0	140		142		126	11	42		2	41	149	148	49
CPU time		2000 s		13000 s	750 s	7300 s	3600 s				2700 s	140 s				700 s			1800 s		460 s		0 s	3800 s	0 s	0 s	660 s				0 s	7600 s		1800 s		19000 s	2000 s	8800 s		150 s	6600 s	6100 s	3800 s	1100 s
ReachSafety-Combinations 671 tasks, max. score: 912		63		222	215	347	328				303	23				44			301	0	0		0	244	0						0	304		119		223	26	91		31	122	188	232	258
CPU time		1500 s		31000 s	32000 s	82000 s	75000 s				70000 s	910 s				10000 s			21000 s	0 s	0 s		0 s	50000 s	0 s						0 s	37000 s		2600 s		13000 s	1200 s	13000 s		1100 s	25000 s	65000 s	48000 s	14000 s
ReachSafety-Hardware 1222 tasks, max. score: 1950		168		100	34	-12590	-10293				281	-832				-764			214	0			50	179	-2352	-7984					56	9		20		117	155	108		0	103	158	-104	25
CPU time		2800 s		24000 s	38 s	4100 s	2000 s				61000 s	0 s				1000 s			860 s	0 s			87 s	16000 s	19000 s	0 s					30 s	24000 s		3.7 s		14000 s	3600 s	9700 s		0 s	8800 s	8900 s	12000 s	230 s
MemSafety 3202 tasks, max. score: 4543		611		-4655	1798		2539		2587		2612					-354			2000						2179						556				1926	2620		2301		1526	2354
CPU time		460 s		6500 s	2300 s		30000 s		20000 s		22000 s					53 s			39000 s						92000 s						1500 s				2100 s	5000 s		220000 s		71000 s	120000 s
MemSafety-Arrays 43 tasks, max. score: 63		10		5	3		24		4		4					0			18				0	4	12						10	4			5	19		41		25	39
CPU time		13 s		910 s	3.4 s		110 s		16 s		17 s					0 s			3.4 s				0 s	16 s	230 s						7.0 s	26 s			4.5 s	250 s		980 s		620 s	920 s
MemSafety-Heap 153 tasks, max. score: 225		15		148	45		87		143		150					-70			119				0	148	97						26	150			165	181		83		78	80
CPU time		110 s		660 s	570 s		2300 s		780 s		800 s					20 s			800 s				0 s	710 s	1600 s						12 s	1100 s			1700 s	1300 s		4900 s		5000 s	4200 s
MemSafety-LinkedLists 79 tasks, max. score: 131		39		79	80		83		80		67					42			58				0	67	12						2	67			105	113		4		4	4
CPU time		330 s		72 s	240 s		1400 s		490 s		500 s					30 s			440 s				0 s	540 s	150 s						0.96 s	610 s			54 s	1200 s		150 s		890 s	160 s
MemSafety-Other 38 tasks, max. score: 53		29		22	21		35		19		22					-28			19				0	22	31						4	22			35	48		39		8	43
CPU time		2.5 s		850 s	14 s		4700 s		440 s		120 s					2.8 s			290 s				0 s	110 s	410 s						2.4 s	160 s			320 s	2200 s		1200 s		2500 s	1000 s
MemSafety-Juliet 2828 tasks, max. score: 4266		0		4152	3560		4180		4021		4266					0			3727				0	4266	4235						1440	4266			0	0		3017		2221	3186
CPU time		0 s		4000 s	1400 s		21000 s		18000 s		20000 s					0 s			38000 s				0 s	21000 s	89000 s						1400 s	27000 s			0 s	0 s		210000 s		59000 s	120000 s
MemSafety-MemCleanup 61 tasks, max. score: 62		-27		-784	11		11		54		54					0			0				0	0	43						0	54			10	36		41		44	41
CPU time		5.7 s		0 s	5.3 s		110 s		310 s		310 s					0 s			0 s				0 s	0 s	1300 s						0 s	450 s			2.8 s	31 s		1900 s		3400 s	1800 s
ConcurrencySafety 2865 tasks, max. score: 5295		0		9	1185	59	847			-2720	1744		-11702	1268	4744	-2	-317	480	1162				1591		118	-5737		-13840	1023				552			194	1286	2717	2710	0	2612
CPU time		0 s		9.2 s	6800 s	2200 s	74000 s			1600 s	57000 s		55000 s	25000 s	3800 s	31000 s	170000 s	59000 s	91000 s				1600 s		2800 s	920 s		30000 s	48000 s				21000 s			10000 s	78000 s	120000 s	130000 s	0 s	80000 s
ConcurrencySafety-Main 665 tasks, max. score: 999		0		2	479	17	315			-740	493		604	525	835	-2	369	-30	346				82	411	108	-5268		518	450			492	524			174	121	579	609	0	585
CPU time		0 s		0.46 s	4100 s	670 s	25000 s			380 s	25000 s		14000 s	14000 s	460 s	31000 s	160000 s	12000 s	2100 s				26 s	25000 s	2600 s	4.4 s		8000 s	5400 s			26000 s	21000 s			10000 s	8900 s	31000 s	26000 s	0 s	27000 s
ConcurrencySafety-MemSafety 705 tasks, max. score: 1410		0		2	0	4	284			0	-16		-4340	0	1316	0	0	298	430				0	-16	-16	266		-4384	268			-16				2	480	332	338	0	338
CPU time		0 s		0.48 s	0 s	110 s	24000 s			0 s	0 s		14000 s	0 s	960 s	0 s	0 s	22000 s	41000 s				0 s	0 s	0 s	450 s		7300 s	17000 s			0 s				0.57 s	24000 s	7600 s	10000 s	0 s	7400 s
ConcurrencySafety-NoOverflows 712 tasks, max. score: 1417		0		5	665	36	218			0	858		-4404	0	1392	0	0	208	350				308	4	18	680		-4448	264			858				5	478	1058	1035	0	1072
CPU time		0 s		8.3 s	2700 s	1400 s	25000 s			0 s	12000 s		13000 s	0 s	230 s	0 s	0 s	25000 s	48000 s				160 s	27 s	220 s	220 s		7300 s	26000 s			13000 s				4.8 s	28000 s	28000 s	31000 s	0 s	25000 s
NoDataRace-Main 783 tasks, max. score: 1488				0							400		-3840	768	1211								1304		0					226							205	756	732	0	612
CPU time				0 s							20000 s		14000 s	12000 s	2200 s								1400 s		0 s					15 s							17000 s	55000 s	62000 s	0 s	21000 s
NoOverflows 6618 tasks, max. score: 10200		6570		5005	6267		-3793				4079	1316				0			6342	1522			5306		-17785	-77220					5671			-879		2407		8639		7305	8492			-500
CPU time		3200 s		28000 s	23000 s		30000 s				4600 s	3500 s				0 s			17000 s	3500 s			530 s		1600 s	1300 s					3800 s			160 s		1800 s		190000 s		120000 s	200000 s			1300 s
NoOverflows-Main 576 tasks, max. score: 917		612		320	351		731				710	229				0			350	-148			402	707	57	-6284					422	710		-153		419		758		654	752			-87	-560
CPU time		440 s		1500 s	230 s		3900 s				4600 s	3500 s				0 s			380 s	33 s			40 s	4600 s	1600 s	75 s					260 s	5700 s		160 s		1800 s		13000 s		10000 s	13000 s			1300 s	0 s
NoOverflows-Juliet 6042 tasks, max. score: 9006		5576		5782	7761		-14594				0	0				0			7908	4332			5472	0	-33072	-75082					5928	0		0		0		7824		6478	7618			0
CPU time		2700 s		26000 s	23000 s		26000 s				0 s	0 s				0 s			16000 s	3500 s			480 s	0 s	0 s	1200 s					3500 s	0 s		0 s		0 s		180000 s		110000 s	180000 s			0 s
Termination 1809 tasks, max. score: 3103		1183		195	862		947				883					0			782						590									631		930		2105		0	0			2305
CPU time		13000 s		26000 s	9600 s		18000 s				35000 s					0 s			3900 s						12000 s									630 s		14000 s		47000 s		0 s	0 s			76000 s
Termination-BitVectors 34 tasks, max. score: 57		28		32	26		27				7					0			24				0	-121	20							7		26		26		39		0	0			46
CPU time		3.7 s		56 s	4.4 s		74 s				17 s					0 s			4.7 s				0 s	24 s	210 s							28 s		3.1 s		34 s		540 s		0 s	0 s			41 s
Termination-MainControlFlow 277 tasks, max. score: 488		256		76	64		29				283					0			64				0	180	212							283		56		62		379		0	0			340
CPU time		55 s		3300 s	55 s		1900 s				1800 s					0 s			950 s				0 s	2800 s	3200 s							2200 s		72 s		79 s		5100 s		0 s	0 s			910 s
Termination-MainHeap 37 tasks, max. score: 70		0		-62	2		2				0					0			2				0	0	-14							0		2		2		43		0	0			54
CPU time		0 s		3.7 s	0.34 s		2.9 s				0 s					0 s			0.24 s				0 s	0 s	28 s							0 s		0.084 s		0.46 s		1200 s		0 s	0 s			140 s
Termination-Other 1461 tasks, max. score: 2237		1268		1303	1250		1667				1060					0			1080				0	1187	482							1060		548		1481		1428		0	0			1545
CPU time		13000 s		23000 s	9500 s		16000 s				33000 s					0 s			3000 s				0 s	54000 s	8800 s							35000 s		560 s		14000 s		40000 s		0 s	0 s			75000 s
SoftwareSystems 3173 tasks, max. score: 5132		75		1589	-711		1421	458	804		758					101			275				358	-1186	-1337	-25556					815	812				1604		476		274	412
CPU time		58 s		1100 s	4300 s		92000 s	80000 s	85000 s		160000 s					8900 s			24000 s				30000 s	77000 s	54000 s	250 s					43000 s	170000 s				2900 s		120000 s		59000 s	110000 s
SoftwareSystems-AWS-C-Common-ReachSafety 165 tasks, max. score: 323		22		163	-12	0	57	0	20		75	-399				8			19				36	62	8						32	60				177		70		4	34
CPU time		5.7 s		220 s	120 s	2800 s	1100 s	410 s	250 s		2800 s	73 s				220 s			250 s				5.5 s	3100 s	190 s						18 s	5100 s				270 s		3800 s		66 s	1600 s
SoftwareSystems-BusyBox-ReachSafety 5 tasks, max. score: 5		0		0	0	0	0	0	0		0					0			0				0	-32	-32	0					0	1				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	0 s	0 s					0 s	57 s				0 s		0 s		0 s	0 s
SoftwareSystems-BusyBox-MemSafety 31 tasks, max. score: 55		0		5	-62		0	0	0		0					0			0					0	0	-379					0	0				4		0		0	0
CPU time		0 s		28 s	71 s		0 s	0 s	0 s		0 s					0 s			0 s					0 s	0 s	14 s					0 s	0 s				51 s		0 s		0 s	0 s
SoftwareSystems-BusyBox-NoOverflows 58 tasks, max. score: 83		0		-15	0		0	0	0		4	-32				0			0	0			0	4	2	-558					4	4				0		4		4	4
CPU time		0 s		260 s	0 s		0 s	0 s	0 s		1200 s	0 s				0 s			0 s	0 s			0 s	1100 s	510 s	0.37 s					2.1 s	1200 s				0 s		120 s		170 s	530 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 2418 tasks, max. score: 4597		304		75	-5129	741	2497	3231	3233		2760	-22428				728			1898				2476	2960	818						3174	2952				1350		2774		2043	2767
CPU time		53 s		140 s	190 s	66000 s	86000 s	80000 s	84000 s		150000 s	43 s				8700 s			23000 s				30000 s	72000 s	51000 s						43000 s	160000 s				1600 s		120000 s		59000 s	110000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety 8 tasks, max. score: 16		0		0	0	0	0	2	2		0	-96				0			0				0	0	0						10	0				0		0		0	0
CPU time		0 s		0 s	0 s	0 s	0 s	330 s	320 s		0 s	0 s				0 s			0 s				0 s	0 s	0 s						20 s	0 s				0 s		0 s		0 s	0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety 94 tasks, max. score: 94		0		43	3		25	0	36		25					0			5					-7	14						0	25				-31		1		1	1
CPU time		0 s		130 s	48 s		530 s	0 s	440 s		290 s					0 s			680 s					280 s	540 s						0 s	350 s				31 s		51 s		34 s	50 s
SoftwareSystems-OpenBSD-MemSafety 4 tasks, max. score: 5		0		4	4		2	0	0		0					0			0					0	2	-15					0	0				4		0		0	0
CPU time		0 s		6.2 s	2.5 s		58 s	0 s	0 s		0 s					0 s			0 s					0 s	15 s	4.5 s					0 s	0 s				56 s		0 s		0 s	0 s
SoftwareSystems-uthash-ReachSafety 138 tasks, max. score: 276		0		228	0	0	228	0	0		0	60				0			0				0	0	0	-2208					0	0				228		0		0	0
CPU time		0 s		110 s	0 s	0 s	880 s	0 s	0 s		0 s	8.1 s				0 s			0 s				0 s	0 s	0 s	0 s					0 s	0 s				79 s		0 s		0 s	0 s
SoftwareSystems-uthash-MemSafety 138 tasks, max. score: 204		0		204	96		156	0	96		96					0			0					96	96	-2172					0	96				204		0		0	0
CPU time		0 s		250 s	3900 s		3600 s	0 s	520 s		530 s					0 s			0 s					640 s	1900 s	180 s					0 s	650 s				810 s		0 s		0 s	0 s
SoftwareSystems-uthash-NoOverflows 114 tasks, max. score: 228		0		0	0		0	0	0		0	0				0			0	0			0	0	0	-480					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	0 s	0 s	0 s					0 s	0 s				0 s		0 s		0 s	0 s
FalsificationOverall 21996 tasks, max. score: 8689		1884		4313	2110		3734				4254					-573			3507					3447	-3063							4258				4026		4173		3092	4100
CPU time		30000 s		130000 s	110000 s		240000 s				320000 s					120000 s			78000 s					170000 s	65000 s							170000 s				55000 s		220000 s		79000 s	170000 s
Overall 23805 tasks, max. score: 38644		9722		2426	10886		7212				14559					1429			13299				6397	5258	-8217							14652				12097		19589		8102	14514
CPU time		110000 s		190000 s	170000 s		560000 s				810000 s					170000 s			310000 s				32000 s	360000 s	200000 s							580000 s				140000 s		890000 s		350000 s	670000 s
JavaOverall 586 tasks, max. score: 827																																														-2816	652	400	220	667	382	495	182
CPU time																																														710 s	11000 s	14000 s	5500 s	1200 s	1800 s	1400 s	1400 s
ReachSafety-Java 586 tasks, max. score: 827																																														-2816	652	400	220	667	382	495	182
CPU time																																														710 s	11000 s	14000 s	5500 s	1200 s	1800 s	1400 s	1400 s
Participants	Plots	2LS	BRICK	Bubaak	CBMC	CoVeriTeam-Verifier-AlgoSelection	CoVeriTeam-Verifier-ParallelPortfolio	CPA-BAM-BnB	CPA-BAM-SMG	CPALockator	CPAchecker	Crux	CSeq	Dartagnan	Deagle	DIVINE	EBF	ESBMC-incr	ESBMC-kind	Frama-C-SV	Gazer-Theta	GDart-LLVM	Goblint	Graves-CPA	Graves-Par	Infer	Korn	Lazy-CSeq	LF-checker	Locksmith	Mopsa	PeSCo-CPA	PIChecker	Pinaka	PredatorHP	Symbiotic	Theta	UAutomizer	UGemCutter	UKojak	UTaipan	VeriAbs	VeriAbsL	VeriFuzz	VeriOover	COASTAL	GDart	Java-Ranger	JayHorn	JBMC	JDart	MLB	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).