TACAS 2024
13th Competition on Software Verification (SV-COMP 2024)

Results of the Competition

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

• Competition Report of SV-COMP 2024
• 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 2024 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. VeriAbsL 2. VeriAbs 3. CPAchecker	MemSafety 1. PredatorHP 2. Symbiotic 3. UAutomizer	ConcurrencySafety 1. Dartagnan 2. UGemCutter 3. UAutomizer
NoOverflows 1. UAutomizer 2. UTaipan 3. CPAchecker	Termination 1. PROTON 2. UAutomizer 3. 2LS	SoftwareSystems 1. Mopsa 2. Bubaak-SpLit 3. CPAchecker
FalsificationOverall 1. CPAchecker 2. Symbiotic 3. UTaipan	Overall 1. UAutomizer 2. CPAchecker 3. UTaipan
JavaOverall 1. MLB 2. JBMC 3. GDart

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.

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.

*) The verifier Deagle has been disqualified from several categories because the verifier uses identifiers contained in the verification task to identify groups of tasks to set parameters of the verification engine. More precisely: (a) Deagle identifies the presence of variables named “threads_total” here. (b) In such cases, it uses a special unwinding limit here. (c) In such cases, it does not generate unwinding assumptions here and here.

Hide base categories

Participants	Plots	2LS	aise	BRICK	Bubaak	Bubaak-SpLit	CBMC	CoVeriTeam-Verifier-AlgoSelection	CoVeriTeam-Verifier-ParallelPortfolio	CPA-BAM-BnB	CPA-BAM-SMG	CPALockator	CPAchecker	CPV	Crux	CSeq	Dartagnan	Deagle	DIVINE	EBF	EmergenTheta	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	PROTON	sv-sanitizers	Symbiotic	Theta	UAutomizer	UGemCutter	UKojak	UTaipan	VeriAbs	VeriAbsL	VeriOover	COASTAL	GDart	Java-Ranger	JayHorn	JBMC	JDart	MLB	SPF	SWAT
Representing Jury Member		Viktor Malík	Zhenbang Chen	Lei Bu	Marek Chalupa	Marek Chalupa	Hors Concours	Hors Concours	Hors Concours	Hors Concours	Hors Concours	Hors Concours	Daniel Baier	Po-Chun Chien	Hors Concours	Hors Concours	Hernán Ponce de León	Fei He	Hors Concours	Fatimah Aljaafari	Levente Bajczi	Hors Concours	Franz Brauße	Martin Spiessl	Hors Concours	Hors Concours	Simmo Saan	Hors Concours	Hors Concours	Hors Concours	Gidon Ernst	Hors Concours	Hors Concours	Hors Concours	Raphaël Monat	Hors Concours	Hors Concours	Hors Concours	Veronika Šoková	Ravindra Metta	Simmo Saan	Martin Jonáš	Levente Bajczi	Matthias Heizmann	Dominik Klumpp	Frank Schüssele	Daniel Dietsch	Priyanka Darke	Priyanka Darke	Hors Concours	Hors Concours	Falk Howar	Hors Concours	Hassan Mousavi	Peter Schrammel	Hors Concours	Lei Bu	Hors Concours	Nils Loose
Affiliation		Brno University of Technology, Czechia	National University of Defense Technology, China	Nanjing University, China	ISTA, Austria	ISTA, Austria	--, --	--, --	--, --	--, --	--, --	--, --	LMU Munich, Germany	LMU Munich, Germany	--, --	--, --	Huawei Dresden Research Center, Germany	Tsinghua University, China	--, --	University of Manchester, UK	Budapest University of Technology and Economics, Hungary	--, --	University of Manchester, UK	LMU Munich, Germany	--, --	--, --	University of Tartu, Estonia	--, --	University of Virginia, USA	--, --	LMU Munich, Germany	--, --	--, --	--, --	Inria and University of Lille, France	--, --	--, --	--, --	Brno University of Technology, Czechia	TCS, India	University of Tartu, Estonia	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	--, --	--, --	TU Dortmund, Germany	--, --	University of Tehran, Tehran Institute for Advanced Studies, Iran	University of Sussex and Diffblue, UK	--, --	Nanjing University, China	--, --	University of Luebeck, Germany
ReachSafety 11222 valid tasks (8323 true, 2899 false, 83 void), max. score: 17746		6000			3788	4692	1269	2635	-6152				10084	6330	2066				4655		1178		8364				2289	3831	876	-99128					2241	5814		2418				7052	2119	6320		4869	5751	10541	10735
CPU time		110000 s			110000 s	45000 s	150000 s	370000 s	280000 s				730000 s	390000 s	7500 s				180000 s		79000 s		180000 s				440 s	230000 s	200000 s	60 s					40000 s	580000 s		28000 s				140000 s	85000 s	280000 s		220000 s	240000 s	680000 s	690000 s
ReachSafety-Arrays 433 valid tasks (320 true, 113 false, 0 void), max. score: 753		0		179	214	122	-52	285	241				76	76	-192				59		26		115	0			52	68	0	-4706					10	126		125				218	21	90		83	92	722	695
CPU time		1100 s		560 s	1900 s	200 s	2400 s	14000 s	3900 s				9300 s	2000 s	120 s				2900 s		910 s		3300 s	0 s			13 s	2500 s	0 s	3.9 s					5.2 s	1400 s		2100 s				2600 s	1000 s	2200 s		3100 s	5500 s	14000 s	18000 s
ReachSafety-BitVectors 49 valid tasks (34 true, 15 false, 0 void), max. score: 83		45		49	49	34	25	49	28				67	76	44				42		23		55	0	57	32	22	55	37	-654					12	72		40				49	33	55		40	50	71	71
CPU time		240 s		690 s	1100 s	120 s	6.3 s	1800 s	3900 s				4400 s	8500 s	57 s				780 s		770 s		530 s	0 s	210 s	1900 s	1.3 s	1700 s	950 s	0.30 s					8.7 s	3100 s		73 s				1100 s	980 s	2200 s		1700 s	3800 s	3500 s	2400 s
ReachSafety-ControlFlow 66 valid tasks (37 true, 29 false, 0 void), max. score: 103		30			-215	20	-242	-241	-482				44	32	-22				32		13		-32		-167		26	-89	-207	-672	32				8	-317		-187				36	16	41		43	43	43	46
CPU time		8.1 s			1900 s	1500 s	40 s	720 s	1300 s				3200 s	65 s	9.2 s				240 s		2800 s		35 s		150 s		1.6 s	1300 s	910 s	0 s	260 s				27 s	880 s		5.3 s				2900 s	500 s	1200 s		1700 s	880 s	1300 s	1100 s
ReachSafety-ECA 1263 valid tasks (783 true, 480 false, 0 void), max. score: 2046		541			278	77	308	155	245				1010	1144	10				147		2		1067	0	369		0	652	1	-12432					2	990		261				273	423	956		370	371	1212	1252
CPU time		73000 s			4600 s	370 s	75000 s	39000 s	21000 s				160000 s	130000 s	320 s				55000 s		25 s		70000 s	0 s	26000 s		0 s	59000 s	36 s	28 s					4.5 s	64000 s		6900 s				5900 s	32000 s	82000 s		55000 s	21000 s	240000 s	180000 s
ReachSafety-Floats 1072 valid tasks (804 true, 268 false, 8 void), max. score: 1876		642		858	723	529	-254	-480	-3968				757	313	608				260		-48		853		337		42	-312	539						112	790		-70				693	73	555		416	619	733	841
CPU time		3500 s		1900 s	3200 s	310 s	24000 s	43000 s	11000 s				9100 s	25000 s	210 s				10000 s		1500 s		14000 s		340 s		2.4 s	11000 s	11000 s						180 s	11000 s		3200 s				2100 s	2700 s	42000 s		36000 s	38000 s	19000 s	18000 s
ReachSafety-Heap 239 valid tasks (166 true, 73 false, 1 void), max. score: 405		218			292	286	289	243	189				279	112	4				222		4		290				130	280	133	-2348					190	308		229	312			308	4	245		229	190	310	300
CPU time		1200 s			330 s	650 s	100 s	9800 s	730 s				4000 s	600 s	110 s				930 s		5.6 s		840 s				24 s	3500 s	3800 s	4.8 s					130 s	3400 s		13 s	210 s			420 s	14 s	7400 s		7500 s	6400 s	13000 s	6600 s
ReachSafety-Loops 729 valid tasks (528 true, 201 false, 61 void), max. score: 1257		462	847		877	782	402	535	259				793	528	480				725		427		717	0	639		236	549	161	-7810	673				298	708		680				888	276	847		602	843	960	921
CPU time		8800 s	9400 s		35000 s	9300 s	5200 s	28000 s	28000 s				27000 s	58000 s	460 s				20000 s		4500 s		13000 s	0 s	8300 s		52 s	13000 s	7400 s	8.9 s	14000 s				820 s	12000 s		4800 s				40000 s	9500 s	35000 s		34000 s	40000 s	50000 s	35000 s
ReachSafety-ProductLines 597 valid tasks (332 true, 265 false, 0 void), max. score: 929		706			453	225	255	352	252				927	0	223				805		0		605	0	867		380	807	689						640	911		131				517	0	566		317	572	900	910
CPU time		1900 s			2200 s	490 s	390 s	21000 s	27000 s				81000 s	0 s	3100 s				20000 s		0 s		600 s	0 s	23000 s		93 s	9200 s	18000 s						31000 s	17000 s		21 s				17000 s	0 s	13000 s		7500 s	22000 s	98000 s	76000 s
ReachSafety-Recursive 156 valid tasks (102 true, 54 false, 6 void), max. score: 258		0			118	145	124	103	-196				111	72	71				130		0		127	0	108		80	-334	-252	-1444	124				12	136		121				150	59	163		94	151	104	97
CPU time		0 s			2200 s	860 s	270 s	4500 s	1500 s				930 s	450 s	79 s				1100 s		0 s		2300 s	0 s	550 s		140 s	1200 s	62 s	1.5 s	780 s				6.2 s	1600 s		190 s				2800 s	4200 s	10000 s		2800 s	8300 s	2900 s	5500 s
ReachSafety-Sequentialized 584 valid tasks (184 true, 400 false, 0 void), max. score: 768		15			281	58	80	401	316				522	165	-77				-25		1		156				4	387	2	-2752					4	450		234				333	54	39		41	-104	476	533
CPU time		2900 s			9400 s	550 s	3200 s	91000 s	62000 s				69000 s	9300 s	850 s				21000 s		640 s		850 s				1.0 s	16000 s	30 s	0 s					2.2 s	52000 s		2800 s				11000 s	9700 s	12000 s		11000 s	5500 s	65000 s	76000 s
ReachSafety-XCSP 119 valid tasks (60 true, 59 false, 0 void), max. score: 179		148			140	71	165	150	0				153	147	98				9		2		160		148		0	152	148	-928	96				0	146		147				135	46	15		37	44	156	155
CPU time		2100 s			7600 s	12000 s	2000 s	7600 s	0 s				4600 s	680 s	210 s				2200 s		1000 s		2400 s		360 s		0 s	4400 s	4800 s	0 s	790 s				0 s	5300 s		2100 s				5800 s	5200 s	2900 s		7900 s	10000 s	7800 s	4600 s
ReachSafety-Combinations 671 valid tasks (241 true, 430 false, 0 void), max. score: 912		55			201	62	230	359	137				309	266	23				44		0		297	0	13		0	236	0						0	355		119				219	38	103		31	110	139	224
CPU time		1400 s			8700 s	400 s	33000 s	88000 s	44000 s				76000 s	42000 s	960 s				13000 s		0 s		23000 s	0 s	44 s		0 s	51000 s	0 s						0 s	37000 s		3200 s				16000 s	5700 s	15000 s		1200 s	19000 s	37000 s	50000 s
ReachSafety-Hardware 1224 valid tasks (727 true, 497 false, 0 void), max. score: 1951		92			201	101	58	-476	-19				269	247	-9				108		144		188	0			50	179	92	-7616					60	128		20				123	149	152		180	156	211	166
CPU time		2700 s			36000 s	17000 s	170 s	110 s	8800 s				59000 s	21000 s	360 s				1800 s		5200 s		590 s	0 s			110 s	20000 s	11000 s	0 s					41 s	13000 s		3.7 s				18000 s	3400 s	15000 s		15000 s	20000 s	37000 s	44000 s
ReachSafety-Hardness 4005 valid tasks (4005 true, 0 false, 7 void), max. score: 8010		5870			-408	18	262	548	1480				5908	5202	-422				648		746		5774				68	1346	3070	-61324					432	4540		468				212	230	448		486	458	5688	6014
CPU time		15000 s			37 s	18 s	43 s	24000 s	72000 s				210000 s	99000 s	660 s				29000 s		62000 s		48000 s				8.9 s	28000 s	140000 s	5.4 s					7500 s	350000 s		2800 s				13000 s	9700 s	36000 s		40000 s	34000 s	93000 s	170000 s
ReachSafety-Fuzzle 15 valid tasks (0 true, 15 false, 0 void), max. score: 15		0			1	1	1	10	1				14	0	0				0		0		15				0	15	9	0					0	14		1				1	0	8		9	8	0	0
CPU time		0 s			29 s	710 s	6.0 s	2300 s	94 s				3900 s	0 s	0 s				0 s		0 s		470 s				0 s	3100 s	2500 s	0 s					0 s	4700 s		8.1 s				20 s	0 s	740 s		930 s	810 s	0 s	0 s
MemSafety 2080 valid tasks (1850 true, 230 false, 55 void), max. score: 3216		224			1890	1312	1330		1655		2039		1897						298				2077				1304		1627						1516				2321		290	2156		2110		1400	2014
CPU time		1600 s			820 s	1500 s	2600 s		20000 s		14000 s		21000 s						290 s				7500 s				240 s		57000 s						4200 s				4400 s		200 s	2800 s		220000 s		87000 s	130000 s
MemSafety-Arrays 222 valid tasks (185 true, 37 false, 0 void), max. score: 407		12			53	52	-24		33		22		27						12				34				114	23	105						172	23			105		29	152		333		148	265
CPU time		23 s			52 s	110 s	310 s		810 s		190 s		140 s						12 s				32 s				12 s	870 s	1400 s						2000 s	600 s			100 s		9.6 s	110 s		11000 s		9700 s	11000 s
MemSafety-Heap 188 valid tasks (94 true, 94 false, 0 void), max. score: 282		20			204	135	97		81		197		100						-58				196				36	178	149						40	182			218		73	144		107		90	103
CPU time		130 s			230 s	310 s	690 s		4100 s		1600 s		2800 s						150 s				1900 s				2.1 s	1100 s	3100 s						460 s	1500 s			2400 s		58 s	400 s		7200 s		7100 s	6100 s
MemSafety-LinkedLists 103 valid tasks (75 true, 28 false, 31 void), max. score: 178		84			124	119	127		123		127		126						84				128				2	114	37						58	114			160		17	130		18		9	12
CPU time		1300 s			41 s	71 s	300 s		1500 s		730 s		860 s						64 s				480 s				0.11 s	770 s	1400 s						45 s	890 s			100 s		130 s	200 s		1700 s		1700 s	3000 s
MemSafety-Other 112 valid tasks (80 true, 32 false, 0 void), max. score: 192		27			118	-18	60		117		135		136						52				156				116	68	76						142	72			134		19	119		174		113	170
CPU time		9.6 s			64 s	81 s	39 s		4400 s		1600 s		1000 s						63 s				180 s				10 s	430 s	1600 s						89 s	1500 s			820 s		5.7 s	740 s		4500 s		6300 s	3700 s
MemSafety-Juliet 1414 valid tasks (1414 true, 0 false, 0 void), max. score: 2828		0			2752	2752	2828		2828		2676		2828						0				2828				2698	2828	2804						2224	2828			2752		0	2752		2506		1834	2766
CPU time		0 s			430 s	920 s	1300 s		8700 s		9900 s		16000 s						0 s				4900 s				220 s	12000 s	49000 s						1700 s	14000 s			860 s		0 s	1300 s		200000 s		60000 s	110000 s
MemSafety-MemCleanup 41 valid tasks (2 true, 39 false, 24 void), max. score: 43		-26			4	4	-10		7		35		34						0				19				0	0	24						0	35			36		0	41		26		27	23
CPU time		180 s			0.35 s	1.1 s	1.3 s		67 s		230 s		260 s						0 s				13 s				0 s	0 s	770 s						0 s	300 s			92 s		0 s	47 s		1400 s		2300 s	1000 s
ConcurrencySafety 3129 valid tasks (2550 true, 579 false, 130 void), max. score: 5672		0			11	7	1229	41	911			-4924	2029			-12478	3547	*)	390	636		542	1853				2583		53	-8289		-15024	772				521					238	2354	3079	3189	0	2655
CPU time		0 s			4.4 s	1.7 s	10000 s	1600 s	70000 s			2100 s	73000 s			52000 s	51000 s		34000 s	250000 s		49000 s	76000 s				2100 s		2900 s	960 s		22000 s	41000 s				23000 s					250 s	27000 s	100000 s	120000 s	0 s	84000 s
ConcurrencySafety-Main 685 valid tasks (348 true, 337 false, 27 void), max. score: 1033		0			2	2	453	8	213			-1707	454			586	581	883	341	389		-130	213				90	398	72	-5178		504	116			462	481					-20	382	545	618	0	512
CPU time		0 s			0.23 s	0.56 s	6000 s	290 s	22000 s			340 s	29000 s			12000 s	11000 s	1000 s	34000 s	160000 s		4500 s	10000 s				59 s	30000 s	2800 s	5.5 s		5900 s	3700 s			9600 s	23000 s					28 s	9800 s	28000 s	20000 s	0 s	22000 s
ConcurrencySafety-MemSafety 738 valid tasks (724 true, 14 false, 29 void), max. score: 1462		0			2	2	2	4	324			0	0			-4544	921	1284	0	0		356	819				952	-32	-32	631		-4584	328			-32					-15	0	644	339	351	0	345
CPU time		0 s			0.23 s	0.56 s	2.9 s	110 s	23000 s			0 s	0 s			11000 s	13000 s	1200 s	0 s	0 s		21000 s	2200 s				740 s	0 s	0 s	530 s		3900 s	16000 s			0 s					6.9 s	0 s	4100 s	8600 s	8100 s	0 s	7900 s
ConcurrencySafety-NoOverflows 733 valid tasks (726 true, 7 false, 34 void), max. score: 1459		0			6	2	667	26	304			0	1002			-4448	950	1306	0	0		294	589				370	4	4	892		-4488	274			1002						246	658	1049	1077	0	1073
CPU time		0 s			4.0 s	0.58 s	4000 s	1200 s	25000 s			0 s	16000 s			9900 s	13000 s	1100 s	0 s	0 s		23000 s	48000 s				350 s	32 s	140 s	210 s		4000 s	22000 s			16000 s						220 s	4900 s	21000 s	28000 s	0 s	22000 s
NoDataRace-Main 973 valid tasks (752 true, 221 false, 40 void), max. score: 1725					0	0							554			-4472	1112	*)					141				1338		0					162							68		664	1220	1200	0	700
CPU time					0 s	0 s							28000 s			19000 s	14000 s						15000 s				900 s		0 s					14 s							1200 s		8000 s	42000 s	60000 s	0 s	32000 s
NoOverflows 8113 valid tasks (4507 true, 3606 false, 75 void), max. score: 13044		5976			6465	-41374	5771		-17812				8603		490				0				8272	1098			7059		-17650	-73312					8063			1337				7370		9497		7363	9231
CPU time		7300 s			36000 s	3700 s	22000 s		16000 s				66000 s		8900 s				0 s				48000 s	3600 s			870 s		110000 s	1400 s					7600 s			4200 s				57000 s		220000 s		150000 s	240000 s
NoOverflows-Main 1881 valid tasks (1429 true, 452 false, 75 void), max. score: 3310		1445			1245	-598	591		-951				2075		234				0				1332	-644			1512	1414	852	-11390					1920	2075		639				1666		2653		1806	2581			424
CPU time		4500 s			25000 s	1100 s	2100 s		15000 s				21000 s		8900 s				0 s				7400 s	290 s			340 s	21000 s	25000 s	270 s					2800 s	21000 s		4200 s				9700 s		78000 s		61000 s	91000 s			5600 s
NoOverflows-Juliet 6232 valid tasks (3078 true, 3154 false, 0 void), max. score: 9310		4493			5874	-61076	6902		-24084				6485		0				0				8348	3724			5928	0	-29582	-75308					6156	5542		0				5911		6004		5454	5828
CPU time		2900 s			12000 s	2500 s	20000 s		700 s				45000 s		0 s				0 s				41000 s	3300 s			530 s	0 s	84000 s	1200 s					4900 s	41000 s		0 s				48000 s		140000 s		87000 s	150000 s
Termination 2298 valid tasks (1480 true, 818 false, 56 void), max. score: 4000		1584			1481	661	1125		1289				1195						0				1048				890		1256									855		3526		1258		3248		0	0
CPU time		15000 s			24000 s	570 s	17000 s		23000 s				99000 s						0 s				3800 s				18000 s		26000 s									2200 s		69000 s		17000 s		64000 s		0 s	0 s
Termination-BitVectors 36 valid tasks (22 true, 14 false, 1 void), max. score: 58		34			36	14	24		27				15						0				24				2	-116	27							5		24		53		27		52		0	0
CPU time		4.7 s			100 s	21 s	3.8 s		87 s				360 s						0 s				8.2 s				0.16 s	67 s	460 s							20 s		3.2 s		2700 s		28 s		730 s		0 s	0 s
Termination-MainControlFlow 294 valid tasks (220 true, 74 false, 0 void), max. score: 514		272			115	38	68		58				223						0				66				126	172	271							245		56		438		89		409		0	0
CPU time		120 s			1300 s	19 s	720 s		3000 s				38000 s						0 s				1200 s				11 s	3400 s	5000 s							2600 s		79 s		21000 s		580 s		6100 s		0 s	0 s
Termination-MainHeap 202 valid tasks (189 true, 13 false, 0 void), max. score: 391		0			48	16	24		26				0						0				22				96	0	-10							0		24		352		24		336		0	0
CPU time		0 s			97 s	8.7 s	15 s		79 s				0 s						0 s				8.3 s				7.1 s	0 s	82 s							0 s		1.9 s		18000 s		9.4 s		7500 s		0 s	0 s
Termination-Other 1766 valid tasks (1049 true, 717 false, 55 void), max. score: 2815		1544			1665	976	1662		2066				1579						0				1454				1010	1431	969							1230		902		2416		1796		1928		0	0
CPU time		15000 s			22000 s	520 s	16000 s		20000 s				61000 s						0 s				2500 s				18000 s	55000 s	20000 s							41000 s		2200 s		27000 s		17000 s		50000 s		0 s	0 s
SoftwareSystems 3458 valid tasks (2762 true, 696 false, 355 void), max. score: 5251		10			-1082	872	-2569		-1297	-2439	-2804		784						76				-1063				536	-322	-2037	-24917					2197	-76						687		261		233	351
CPU time		72 s			84000 s	1500 s	5800 s		64000 s	96000 s	99000 s		150000 s						9600 s				24000 s				19000 s	87000 s	57000 s	1400 s					53000 s	150000 s						16000 s		140000 s		99000 s	180000 s
SoftwareSystems-AWS-C-Common-ReachSafety 197 valid tasks (101 true, 96 false, 144 void), max. score: 298		-36			46	18	74	-41	-232	3	28		97	0	-255				-20				111				42	114	92						36	51						137		-135		-96	-79
CPU time		10 s			340 s	220 s	140 s	1900 s	600 s	400 s	250 s		2700 s	0 s	81 s				480 s				640 s				6.9 s	3100 s	2400 s						29 s	1700 s						1200 s		3600 s		1000 s	4200 s
SoftwareSystems-coreutils-MemSafety 140 valid tasks (30 true, 110 false, 0 void), max. score: 170		0			-160	0	-144		-448	0	-288		0						0				-144				0	-288	-288	-464					0	-320					-16	-128		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
SoftwareSystems-coreutils-NoOverflows 30 valid tasks (30 true, 0 false, 0 void), max. score: 60		0			-160	0	-112		-48	0	0		0		0				0				0	0			0	0	-96	-480					4	0						-16		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					240 s	0 s						0 s		0 s		0 s	0 s
SoftwareSystems-BusyBox-NoOverflows 54 valid tasks (21 true, 33 false, 13 void), max. score: 75		0			2	0	0		0	0	0		0		-32				0				0	0			0	0	0	-320					8	0						0		4		4	4
CPU time		0 s			15 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					1100 s	0 s						0 s		120 s		190 s	260 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 2442 valid tasks (2211 true, 231 false, 20 void), max. score: 4653		306			630	85	-5170	406	713	3340	3325		3105	6	-22571				732				2163				2528	3038	818						3476	2878						1426		2812		2316	3106
CPU time		61 s			83000 s	120 s	220 s	62000 s	56000 s	96000 s	98000 s		150000 s	470 s	85 s				9100 s				23000 s				19000 s	83000 s	52000 s						49000 s	150000 s						6000 s		140000 s		98000 s	170000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety 8 valid tasks (8 true, 0 false, 0 void), max. score: 16		0			0	0	0	0	0	2	2		0	0	-96				0				0				0	0	0						14	0						0		0		0	0
CPU time		0 s			0 s	0 s	0 s	0 s	0 s	390 s	400 s		0 s	0 s	0 s				0 s				0 s				0 s	0 s	0 s						150 s	0 s						0 s		0 s		0 s	0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety 141 valid tasks (4 true, 137 false, 0 void), max. score: 145		2			67	71	10		29	0	48		24						0				13				8	1	18						8	32					1	61		2		2	2
CPU time		0.59 s			260 s	780 s	120 s		820 s	0 s	650 s		1400 s						0 s				130 s				1.8 s	710 s	610 s						6.0 s	480 s					0.43 s	7800 s		120 s		88 s	120 s
SoftwareSystems-Other-ReachSafety 22 valid tasks (21 true, 1 false, 9 void), max. score: 43		0			1	1	-32	-32	-31	-288	-288		0	0	0				0				-112				8	-32	-64	-272					10	0						1		0		0	0
CPU time		0 s			0.74 s	1.8 s	0 s	0 s	14 s	0 s	0 s		0 s	0 s	0 s				0 s				0 s				91 s	0 s	0 s	0 s					1200 s	0 s						2.9 s		0 s		0 s	0 s
SoftwareSystems-Other-MemSafety 34 valid tasks (18 true, 16 false, 13 void), max. score: 52		0			-5	-6	-46		-9	0	0		0						0				0				0	0	-15	-293					12	0					8	-4		0		0	0
CPU time		0 s			52 s	56 s	64 s		170 s	0 s	0 s		0 s						0 s				0 s				0 s	0 s	44 s	40 s					440 s	0 s					4.4 s	110 s		0 s		0 s	0 s
SoftwareSystems-uthash-ReachSafety 138 valid tasks (138 true, 0 false, 54 void), max. score: 276		0			228	228	0	0	228	0	0		0	0	60				0				0				0	0	0	-2080					192	0						228		0		0	0
CPU time		0 s			55 s	94 s	0 s	0 s	890 s	0 s	0 s		0 s	0 s	9.9 s				0 s				0 s				0 s	0 s	0 s	0 s					560 s	0 s						97 s		0 s		0 s	0 s
SoftwareSystems-uthash-MemSafety 138 valid tasks (66 true, 72 false, 54 void), max. score: 204		0			204	204	96		174	0	96		144						0				0				0	96	96	-2108					96	96					72	204		0		0	0
CPU time		0 s			110 s	220 s	5300 s		5000 s	0 s	580 s		1700 s						0 s				0 s				0 s	730 s	2100 s	200 s					280 s	700 s					23 s	1200 s		0 s		0 s	0 s
SoftwareSystems-uthash-NoOverflows 114 valid tasks (114 true, 0 false, 48 void), max. score: 228		0			0	0	0		0	0	0		0		0				0				0	0			36	0	0	-464					204	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			32 s	0 s	0 s	0 s					510 s	0 s						0 s		0 s		0 s	0 s
FalsificationOverall 28002 valid tasks (19992 true, 8010 false, 698 void), max. score: 8817		1311			-617	1959	-3764		-9118				4812						256				2394					-1538	-9024							3247						4050		3139		2291	3157
CPU time		34000 s			66000 s	26000 s	150000 s		140000 s				330000 s						140000 s				92000 s					190000 s	77000 s							170000 s						96000 s		140000 s		75000 s	120000 s
Overall 30300 valid tasks (21472 true, 8828 false, 754 void), max. score: 49097		10564			12206	-18177	8391		-7545				21568						3576				17896				15458	5470	-6731							17315						17192		26396		10593	18042
CPU time		140000 s			260000 s	52000 s	200000 s		480000 s				1100000 s						220000 s				340000 s				41000 s	440000 s	460000 s							910000 s						230000 s		1000000 s		560000 s	860000 s
JavaOverall 587 valid tasks (241 true, 346 false, 0 void), max. score: 828																																																			-2752	616	398	325	618	382	676	182	566
CPU time																																																			1200 s	9200 s	14000 s	18000 s	1600 s	2000 s	3400 s	1500 s	5700 s
ReachSafety-Java 587 valid tasks (241 true, 346 false, 0 void), max. score: 828																																																			-2752	616	398	325	618	382	676	182	566
CPU time																																																			1200 s	9200 s	14000 s	18000 s	1600 s	2000 s	3400 s	1500 s	5700 s
Participants	Plots	2LS	aise	BRICK	Bubaak	Bubaak-SpLit	CBMC	CoVeriTeam-Verifier-AlgoSelection	CoVeriTeam-Verifier-ParallelPortfolio	CPA-BAM-BnB	CPA-BAM-SMG	CPALockator	CPAchecker	CPV	Crux	CSeq	Dartagnan	Deagle	DIVINE	EBF	EmergenTheta	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	PROTON	sv-sanitizers	Symbiotic	Theta	UAutomizer	UGemCutter	UKojak	UTaipan	VeriAbs	VeriAbsL	VeriOover	COASTAL	GDart	Java-Ranger	JayHorn	JBMC	JDart	MLB	SPF	SWAT