TACAS 2026
15th Competition on Software Verification (SV-COMP 2026)

Results of the Competition

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

• Competition Report of SV-COMP 2026
• 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 412 and 413.

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 2026 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.
• C.FalseOverall (analogously for C.TrueOverall): 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.

Contents

1. C Verification
2. C.Huawei-Concurrency-Challenges Verification (Demo)
3. Java Verification
4. SV-LIB Verification (Demo)

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.

1. C Verification

Ranking by Category (with Score-Based Quantile Plots)

C.ReachSafety 1. CPAchecker 2. ESBMC-kind 3. Symbiotic	C.MemSafety 1. Symbiotic 2. CPAchecker 3. UAutomizer	C.Concurrency 1. Deagle 2. Dartagnan 3. iekke
C.NoOverflows 1. UParalizer 2. UAutomizer 3. UTaipan	C.Termination 1. PROTON 2. UAutomizer 3. AProVE (KoAT + LoAT)	C.SoftwareSystems 1. Mopsa 2. Symbiotic 3. CPAchecker
C.Overall 1. UAutomizer 2. CPAchecker 3. Symbiotic
C.FalseOverall 1. Symbiotic 2. CPAchecker 3. UAutomizer	C.TrueOverall 1. UAutomizer 2. Goblint 3. Mopsa

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 was not executed in the category.
The definition of the scoring schema can be found in the literature [Proc. TACAS 2024, Fig. 7, page 317] and the categories are defined on the respective SV-COMP web page.

Hide base categories

Participants	Plots	2LS	aise	AProVE (KoAT + LoAT)	BRICK	Bubaak	Bubaak-SpLit	CBMC	CoOpeRace	CPA-BAM-BnB	CPA-BAM-SMG	CPALockator	CPAchecker	CPV	Crux	CSeq	Dartagnan	Deagle	DIVINE	EBF	EmergenTheta	ESBMC-incr	ESBMC-kind	Frama-C-SV	ReFuncTion	Gazer-Theta	GDart-LLVM	Goblint	Goblitch	Graves-CPA	Hornix	iekke	Infer	Korn	Lazy-CSeq	LF-checker	Locksmith	Mopsa	MuVal	Nacpa	OGChecker	PeSCo-CPA	PIChecker	Pinaka	PredatorHP	PROTON	RacerF	Re3ver	SEAL	SV-sanitizers	SVF-SVC	Symbiotic	Theta	Thorn	UAutomizer	UGemCutter	UKojak	UParalizer	UTaipan	VeriAbs	VeriAbsL	VeriOover
Representing Jury Member		inactive	Zhenbang Chen	Nils Lommen	Lei Bu	inactive	inactive	inactive	Vesal Vojdani	inactive	inactive	inactive	Marek Jankola	Po-Chun Chien	inactive	Omar Inverso	Hernán Ponce de León	Fei He	inactive	inactive	Levente Bajczi	Xianzhiyu Li	Xianzhiyu Li	inactive	Naïm Moussaoui Remil	inactive	inactive	Simmo Saan	Karoliine Holter	inactive	Martin Blicha	Paolo Di Biase	inactive	Gidon Ernst	inactive	inactive	inactive	Raphaël Monat	Hiroshi Unno	Henrik Wachowitz	Zuchao Yang	inactive	inactive	inactive	inactive	Ravindra Metta	Tomáš Dacík	Adéla Štěpková	Tomáš Dacík	Simmo Saan	Matthew Richards	Martin Jonáš	Csanád Telbisz	Levente Bajczi	Matthias Heizmann	Dominik Klumpp	Manuel Bentele	Max Barth	Daniel Dietsch	inactive	inactive	inactive
Affiliation			National University of Defense Technology, China	RWTH Aachen, Germany	Nanjing University, China				University of Tartu, Estonia				LMU Munich, Germany	LMU Munich, Germany		Gran Sasso Science Institute, Italy	Huawei Dresden Research Center, Germany	Tsinghua University, China			Budapest University of Technology and Economics, Hungary	University of Manchester, UK	University of Manchester, UK		Inria Paris and École Normale Supérieure, France			University of Tartu, Estonia	University of Tartu, Estonia		Charles University, Czechia	Unimol, Italy		LMU Munich, Germany				Inria and University of Lille, France	Tohoku University, Japan	LMU Munich, Germany	Xidian University, China					Tata Consultancy Services, India	Brno University of Technology, Czechia	Masaryk University, Brno, Czechia	Brno University of Technology, Czechia	University of Tartu, Estonia	University of New South Wales, Australia	Masaryk University, Brno, Czechia	Budapest University of Technology and Economics, Hungary	Budapest University of Technology and Economics, Hungary	University of Freiburg, Germany	University of Freiburg, Germany	University of Freiburg, Germany	LMU Munich, Germany	University of Freiburg, Germany
C.ReachSafety 14375 valid tasks (11308 true, 3067 false, 15 void), max. score: 23331		8100	—	—	—	9071	7959	1896	—	—	—	—	12866	10626	2821	—	—	—	6371	—	4414	—	11037	—	—	—	—	4664	6552	4252	—	—	-131447	—	—	—	—	4501	—	5959	—	8085	—	3818	—	—	—	2583	—	—	-9866	10788	5252	738	8243	—	6012	8279	7013	14056	14404	—
CPU time		130000  s				140000  s	170000  s	140000  s					550000  s	400000  s	8000  s				190000  s		470000  s		200000  s					8200  s	53000  s	240000  s			2500  s					23000  s		410000  s		820000  s		41000  s				110000  s			13000  s	400000  s	400000  s	190000  s	250000  s		230000  s	340000  s	260000  s	780000  s	720000  s
C.unreach-call.Arrays 427 valid tasks (314 true, 113 false, 13 void), max. score: 741		2	—	—	100	208	198	-59	—	—	—	—	59	130	-198	—	—	—	59	—	52	—	110	0	—	—	—	72	122	64	—	—	-4530	152	—	—	—	23	—	89	—	112	—	127	—	—	—	0	—	—	-307	215	104	2	89	—	78	93	78	478	449	—
CPU time		1700  s			200  s	5500  s	14000  s	2000  s					1400  s	7600  s	100  s				2800  s		2500  s		3700  s					73  s	2300  s	1900  s			26  s	1000  s				100  s		1700  s		800  s		1600  s							6  s	2700  s	6200  s	7  s	2500  s		2600  s	3800  s	2500  s	13000  s	14000  s
C.unreach-call.BitVectors 49 valid tasks (34 true, 15 false, 0 void), max. score: 83		45	—	—	0	49	49	35	—	—	—	—	61	76	47	—	—	—	42	—	-10	—	55	0	—	57	32	28	40	59	—	—	-613	—	—	—	—	33	—	65	—	70	—	40	—	—	—	37	—	—	-144	63	-9	-38	61	—	40	61	51	71	71	—
CPU time		220  s				1000  s	660  s	12  s					1800  s	990  s	84  s				740  s		3200  s		530  s			250  s	1800  s	98  s	240  s	1400  s			3  s					81  s		1500  s		2200  s		56  s				3400  s				3200  s	3800  s	470  s	3100  s		1200  s	4000  s	4800  s	3100  s	2000  s
C.unreach-call.Combinations 671 valid tasks (241 true, 430 false, 0 void), max. score: 912		53	—	—	—	185	156	232	—	—	—	—	339	226	23	—	—	—	48	—	36	—	295	0	—	13	—	0	26	236	—	—	—	—	—	—	—	0	—	364	—	384	—	119	—	—	—	26	—	—	0	220	54	-312	56	—	28	76	55	205	233	—
CPU time		1100  s				8300  s	14000  s	30000  s					85000  s	59000  s	890  s				14000  s		5700  s		19000  s			42  s			54  s	45000  s			310  s							96000  s		42000  s		2500  s				890  s				15000  s	14000  s	9000  s	6100  s		960  s	5200  s	6500  s	83000  s	52000  s
C.unreach-call.ControlFlow 73 valid tasks (46 true, 27 false, 2 void), max. score: 119		50	—	—	—	39	35	-228	—	—	—	—	63	52	-13	—	—	—	48	—	44	—	37	—	—	-146	—	60	61	-80	—	—	-762	54	—	—	—	20	—	66	—	-257	—	-154	—	—	—	42	—	—	-79	58	50	40	59	—	57	59	63	46	67	—
CPU time		7  s				4400  s	2500  s	33  s					350  s	180  s	8  s				300  s		7200  s		79  s			780  s		1100  s	120  s	1200  s			8  s	560  s				190  s		280  s		1400  s		26  s				1000  s			0  s	5500  s	1700  s	800  s	1000  s		1400  s	1100  s	1400  s	1400  s	1100  s
C.unreach-call.ECA 1263 valid tasks (783 true, 480 false, 0 void), max. score: 2046		579	—	—	—	317	270	308	—	—	—	—	1216	959	10	—	—	—	153	—	705	—	313	0	—	373	—	56	33	772	—	—	-11610	458	—	—	—	0	—	1225	—	1184	—	261	—	—	—	180	—	—	0	284	668	690	923	—	362	886	405	1326	1368	—
CPU time		76000  s				27000  s	30000  s	67000  s					150000  s	120000  s	320  s				57000  s		52000  s		44000  s			26000  s		390  s	4000  s	61000  s			430  s	47000  s						140000  s		96000  s		4800  s				24000  s				16000  s	190000  s	95000  s	64000  s		60000  s	76000  s	23000  s	230000  s	170000  s
C.unreach-call.Floats 1400 valid tasks (971 true, 429 false, 0 void), max. score: 2371		637	—	—	828	698	662	-785	—	—	—	—	824	350	658	—	—	—	280	—	97	—	1009	—	—	281	—	52	351	-1201	—	—	—	—	—	—	—	114	—	828	—	547	—	-351	—	—	—	16	—	—	0	737	110	0	757	—	514	655	568	768	876	—
CPU time		3300  s			1700  s	4100  s	5200  s	34000  s					12000  s	22000  s	300  s				10000  s		6400  s		21000  s			310  s		57  s	8200  s	11000  s			34  s					420  s		15000  s		13000  s		11000  s				3  s				2100  s	5400  s		51000  s		35000  s	64000  s	36000  s	19000  s	17000  s
C.unreach-call.Hardness 6789 valid tasks (6789 true, 0 false, 0 void), max. score: 13578		8340	—	—	—	4914	190	346	—	—	—	—	8628	8270	-938	—	—	—	1028	—	1522	—	8718	—	—	—	—	26	28	2246	—	—	-104028	—	—	—	—	382	—	-40158	—	7936	—	1096	—	—	—	696	—	—	0	2260	2014	326	664	—	1482	914	1536	11500	11788	—
CPU time		32000  s				14000  s	28000  s	50  s					170000  s	86000  s	1600  s				43000  s		250000  s		96000  s					76  s	1000  s	49000  s			5  s					4300  s		96000  s		550000  s		12000  s				52000  s				210000  s	76000  s	19000  s	47000  s		63000  s	110000  s	80000  s	180000  s	240000  s
C.unreach-call.Hardware 1224 valid tasks (727 true, 497 false, 0 void), max. score: 1951		96	—	—	—	138	139	56	—	—	—	—	327	433	-9	—	—	—	91	—	262	—	114	0	—	—	—	78	87	186	—	—	-7531	—	—	—	—	80	—	450	—	54	—	20	—	—	—	97	—	—	0	148	275	25	122	—	143	122	97	195	160	—
CPU time		1700  s				15000  s	9900  s	120  s					52000  s	6700  s	340  s				1300  s		45000  s		860  s					2100  s	3100  s	23000  s			900  s					360  s		18000  s		16000  s		4  s				11000  s				19000  s	17000  s	3900  s	10000  s		8400  s	13000  s	6300  s	32000  s	41000  s
C.unreach-call.Heap 240 valid tasks (167 true, 73 false, 0 void), max. score: 407		221	—	—	—	276	275	291	—	—	—	—	282	122	6	—	—	—	210	—	52	—	353	—	—	—	—	142	212	283	—	—	-2341	—	—	—	—	239	—	289	—	309	—	229	314	—	—	10	—	—	-670	310	85	-11	248	—	222	250	192	310	300	—
CPU time		1000  s				330  s	440  s	95  s					2500  s	690  s	97  s				960  s		220  s		430  s					16  s	330  s	3000  s			18  s					460  s		690  s		3200  s		12  s	180  s			4  s			3  s	330  s	570  s	150  s	7200  s		6600  s	7700  s	10000  s	12000  s	5200  s
C.unreach-call.Loops 764 valid tasks (555 true, 209 false, 0 void), max. score: 1319		470	982	—	—	845	849	369	—	—	—	—	793	796	490	—	—	—	711	—	558	—	731	0	—	634	—	480	660	549	290	—	-8012	730	—	—	—	491	—	802	—	692	—	677	—	—	—	168	—	—	-642	884	736	698	852	—	615	873	764	941	903	—
CPU time		7500  s	17000  s			32000  s	19000  s	3800  s					15000  s	72000  s	510  s				18000  s		50000  s		11000  s			8500  s		3100  s	18000  s	12000  s	300  s		44  s	21000  s				2900  s		6300  s		11000  s		5600  s				770  s			3  s	39000  s	44000  s	18000  s	26000  s		31000  s	26000  s	35000  s	49000  s	32000  s
C.unreach-call.ProductLines 597 valid tasks (332 true, 265 false, 0 void), max. score: 929		706	—	—	—	287	223	256	—	—	—	—	927	839	211	—	—	—	802	—	0	—	741	0	—	865	—	560	709	791	—	—	—	—	—	—	—	610	—	929	—	907	—	127	—	—	—	0	—	—	-710	797	0	0	609	—	372	617	636	899	907	—
CPU time		1600  s				15000  s	800  s	350  s					17000  s	7700  s	2800  s				18000  s				650  s			23000  s		1000  s	8800  s	7400  s			120  s					12000  s		3000  s		17000  s		19  s							13000  s	63000  s			11000  s		9000  s	14000  s	42000  s	94000  s	65000  s
C.unreach-call.Recursive 174 valid tasks (104 true, 70 false, 0 void), max. score: 278		0	—	—	—	105	87	118	—	—	—	—	130	58	71	—	—	—	131	—	81	—	145	0	—	110	—	116	131	-320	134	—	-1441	112	—	—	—	85	—	142	—	151	—	125	—	—	—	42	—	—	0	150	92	0	146	—	93	148	146	110	100	—
CPU time						2500  s	1700  s	220  s					1700  s	540  s	60  s				1200  s		11000  s		3400  s			810  s		190  s	390  s	3800  s	32  s		370  s	1300  s				1700  s		1800  s		5700  s		190  s				2100  s				3800  s	5900  s		7900  s		2700  s	8800  s	7400  s	5600  s	6100  s
C.unreach-call.Sequentialized 585 valid tasks (185 true, 400 false, 0 void), max. score: 770		11	—	—	—	254	253	76	—	—	—	—	531	164	-120	—	—	—	-26	—	51	—	154	—	—	—	—	4	12	381	—	—	-2527	43	—	—	—	18	—	539	—	453	—	232	—	—	—	3	—	—	-28	327	76	-133	57	—	28	57	-78	455	512	—
CPU time		1800  s				8600  s	26000  s	2700  s					35000  s	13000  s	700  s				21000  s		25000  s		940  s					0  s	260  s	14000  s			150  s	290  s				96  s		26000  s		51000  s		2400  s				560  s			2  s	10000  s	31000  s	40000  s	12000  s		8000  s	8600  s	8000  s	54000  s	65000  s
C.unreach-call.XCSP 119 valid tasks (60 true, 59 false, 0 void), max. score: 179		148	—	—	—	140	141	159	—	—	—	—	151	154	100	—	—	—	9	—	138	—	156	—	—	150	—	0	41	150	137	—	-883	132	—	—	—	0	—	150	—	147	—	147	—	—	—	36	—	—	0	141	141	18	13	—	13	13	7	154	153	—
CPU time		1300  s				7600  s	18000  s	820  s					2500  s	4400  s	190  s				2200  s		8700  s		1600  s			460  s			6100  s	2800  s	1800  s		100  s	2300  s						4000  s		5300  s		1700  s				9900  s				6200  s	7600  s	4800  s	1900  s		1900  s	1800  s	320  s	6300  s	3300  s
C.MemSafety 4145 valid tasks (1989 true, 2156 false, 0 void), max. score: 6529		631	—	—	—	3296	3283	1817	—	—	3039	—	4646	—	—	—	—	—	532	—	642	—	3309	—	—	—	—	2840	—	2106	—	—	—	—	—	—	—	3165	—	3940	—	2904	—	—	4543	—	—	—	—	878	0	4738	695	12	3957	—	2982	—	3517	—	—	—
CPU time		1500  s				3700  s	7400  s	5200  s			23000  s		68000  s						290  s		17000  s		13000  s					1100  s		29000  s								17000  s		8500  s		34000  s			6400  s					2600  s		14000  s	15000  s	430  s	130000  s		110000  s		130000  s
C.valid-memcleanup.Main 66 valid tasks (3 true, 63 false, 0 void), max. score: 69		-26	—	—	—	65	65	14	—	—	59	—	61	—	—	—	—	—	0	—	0	—	43	—	—	—	—	0	—	0	—	—	—	—	—	—	—	2	—	61	—	59	—	—	62	—	—	—	—	5	0	65	0	0	51	—	53	—	47	—	—	—
CPU time		170  s				53  s	130  s	5  s			340  s		420  s										22  s															1  s		53  s		430  s			76  s					1  s		84  s			2300  s		2500  s		1900  s
C.valid-memsafety.Arrays 221 valid tasks (185 true, 36 false, 0 void), max. score: 406		0	—	—	—	53	53	-24	—	—	23	—	131	—	—	—	—	—	12	—	4	—	53	—	—	—	—	106	—	22	—	—	—	—	—	—	—	179	—	53	—	22	—	—	103	—	—	—	—	28	0	293	-12	0	356	—	179	—	262	—	—	—
CPU time						47  s	100  s	260  s			190  s		620  s						12  s		190  s		30  s					8  s		800  s								1900  s		200  s		530  s			90  s					6  s		110  s	81  s		11000  s		14000  s		10000  s
C.valid-memsafety.Heap 348 valid tasks (167 true, 181 false, 0 void), max. score: 515		105	—	—	—	337	334	206	—	—	276	—	319	—	—	—	—	—	-22	—	-94	—	355	—	—	—	—	164	—	137	—	—	—	—	—	—	—	191	—	331	—	206	—	—	302	—	—	—	—	125	0	337	-52	-27	218	—	162	—	208	—	—	—
CPU time		130  s				1600  s	3100  s	2200  s			1900  s		5100  s						200  s		3600  s		4400  s					410  s		1300  s								560  s		1100  s		1900  s			3300  s					940  s		3600  s	1300  s	48  s	8800  s		12000  s		7000  s
C.valid-memsafety.Juliet 3271 valid tasks (1438 true, 1833 false, 0 void), max. score: 4709		0	—	—	—	4090	4090	3851	—	—	4124	—	4709	—	—	—	—	—	0	—	0	—	4641	—	—	—	—	2774	—	4360	—	—	—	—	—	—	—	3788	—	4709	—	4505	—	—	4562	—	—	—	—	1779	0	4611	0	0	3151	—	2280	—	3078	—	—	—
CPU time						1400  s	3600  s	1800  s			19000  s		59000  s										7500  s					270  s		25000  s								14000  s		4700  s		29000  s			2200  s					1700  s		9500  s			99000  s		76000  s		110000  s
C.valid-memsafety.LinkedLists 134 valid tasks (106 true, 28 false, 0 void), max. score: 240		90	—	—	—	114	114	127	—	—	127	—	201	—	—	—	—	—	84	—	0	—	128	—	—	—	—	98	—	114	—	—	—	—	—	—	—	90	—	205	—	114	—	—	220	—	—	—	114	17	0	130	0	0	22	—	10	—	6	—	—	—
CPU time		1200  s				74  s	170  s	260  s			650  s		2200  s						61  s				450  s					290  s		710  s								110  s		1200  s		770  s			110  s				570  s	11  s		140  s			3400  s		2500  s		940  s
C.valid-memsafety.Other 105 valid tasks (90 true, 15 false, 0 void), max. score: 195		35	—	—	—	50	49	-20	—	—	42	—	142	—	—	—	—	—	16	—	124	—	53	—	—	—	—	166	—	39	—	—	—	—	—	—	—	143	—	65	—	41	—	—	133	—	—	—	—	4	0	126	127	10	167	—	154	—	169	—	—	—
CPU time		26  s				440  s	320  s	640  s			1100  s		570  s						12  s		14000  s		170  s					100  s		990  s								110  s		1200  s		1100  s			590  s					1  s		690  s	14000  s	380  s	2100  s		2900  s		2100  s
C.Concurrency 3124 valid tasks (2520 true, 604 false, 53 void), max. score: 5656		0	—	—	—	-191	-191	812	—	—	—	-3540	2146	—	—	-12677	3516	4630	379	351	2636	2435	2410	—	—	—	—	2555	—	238	—	3428	-8297	—	-14183	440	—	0	—	1578	131	1483	382	—	—	—	—	—	—	—	—	42	2157	1247	2986	3189	0	—	2453	—	—	—
CPU time						1  s	4  s	8500  s				1300  s	59000  s			3  s	69000  s	11000  s	29000  s	190000  s	310000  s	45000  s	44000  s					480  s		27000  s		8400  s	920  s		14000  s	40000  s				67000  s	6100  s	43000  s	25000  s									8  s	42000  s	110000  s	100000  s	120000  s			95000  s
C.no-data-race.Concurrency 986 valid tasks (773 true, 213 false, 44 void), max. score: 1759		—	—	—	—	0	0	—	1439	—	—	—	577	—	—	-4222	1186	1352	—	—	1177	—	642	—	—	—	—	1426	—	0	—	412	—	—	—	—	248	0	—	526	—	338	—	—	—	—	1398	—	—	83	—	—	1201	1136	1295	1337	0	—	776	—	—	—
CPU time									41000  s			1100  s	23000  s			1  s	21000  s	3500  s		44000  s	12000  s	11000  s	10000  s					190  s				1400  s	220  s		5100  s		18  s			22000  s		24000  s					2000  s			520  s			8500  s	18000  s	44000  s	58000  s			27000  s
C.no-overflow.Concurrency 668 valid tasks (660 true, 8 false, 1 void), max. score: 1328		0	—	—	—	6	6	588	—	—	—	0	856	—	—	-4144	860	1150	0	0	639	770	770	—	—	—	—	292	—	0	—	1158	635	—	-4234	142	—	0	—	537	—	710	—	—	—	—	—	—	—	38	—	34	717	169	865	913	0	—	833	—	—	—
CPU time						1  s	2  s	3600  s					9400  s				16000  s	2600  s			140000  s	26000  s	26000  s					110  s				1600  s	170  s		2400  s	23000  s				24000  s		13000  s								5  s		8  s	11000  s	44000  s	23000  s	28000  s			32000  s
C.unreach-call.Concurrency 721 valid tasks (371 true, 350 false, 4 void), max. score: 1092		0	—	—	—	-96	-96	115	—	—	—	-1440	488	—	—	-112	593	847	309	375	329	244	246	—	—	—	—	106	—	235	—	418	-5344	—	400	120	—	0	—	478	121	371	368	—	—	—	—	—	—	—	—	2	312	142	575	643	0	—	534	—	—	—
CPU time								4900  s				250  s	22000  s				18000  s	3300  s	29000  s	150000  s	60000  s	6600  s	6500  s					13  s		27000  s		3100  s	88  s		3600  s	2400  s				20000  s	6100  s	6300  s	25000  s									0  s	7000  s	38000  s	28000  s	23000  s			30000  s
C.valid-memsafety.Concurrency 749 valid tasks (716 true, 33 false, 4 void), max. score: 1465		0	—	—	—	-90	-90	0	—	—	—	0	153	—	—	-4188	891	1244	42	0	576	705	705	—	—	—	—	930	—	-16	—	1242	375	—	-4212	138	—	0	—	15	—	-16	—	—	—	—	—	—	—	-14	—	0	28	-4	313	351	0	—	274	—	—	—
CPU time						1  s	2  s						4100  s			2  s	14000  s	1800  s	49  s		97000  s	1000  s	1100  s					170  s				2400  s	450  s		2800  s	15000  s				200  s										1  s			15000  s	8500  s	8200  s	8800  s			6600  s
C.NoOverflows 8218 valid tasks (4544 true, 3674 false, 6 void), max. score: 13281		6808	—	—	—	6483	6472	7173	—	—	—	—	8474	—	602	—	—	—	0	—	1821	—	9109	1579	—	—	—	8658	—	3329	—	—	-77663	—	—	—	—	9906	—	7869	—	8424	—	641	—	—	—	—	—	837	—	8476	2586	-174	10831	—	8821	11049	10645	—	—	—
CPU time		9500  s				51000  s	44000  s	24000  s					72000  s		9000  s						76000  s		80000  s	4100  s				2100  s		22000  s			1400  s					23000  s		16000  s		60000  s		3700  s						1100  s		130000  s	83000  s	25000  s	240000  s		210000  s	320000  s	270000  s
C.no-overflow.Juliet 6232 valid tasks (3078 true, 3154 false, 0 void), max. score: 9310		5499	—	—	—	5684	5667	6944	—	—	—	—	6620	—	0	—	—	—	0	—	0	—	8412	4390	—	—	—	5870	—	0	—	—	-75263	—	—	—	—	7543	—	6622	—	5682	—	0	—	—	—	—	—	911	—	6714	0	0	8130	—	7498	8088	8059	—	—	—
CPU time		1400  s				19000  s	17000  s	15000  s					52000  s										61000  s	3800  s				500  s					1200  s					16000  s		4900  s		38000  s								800  s		110000  s			180000  s		140000  s	230000  s	190000  s
C.no-overflow.Main 1986 valid tasks (1466 true, 520 false, 6 void), max. score: 3452		1538	—	—	—	1322	1322	1254	—	—	—	—	1986	—	291	—	—	—	0	—	880	—	1722	-636	—	—	—	2314	—	1609	—	—	-13552	—	—	—	—	2384	—	1693	—	2261	—	310	—	—	—	—	—	114	—	1957	1250	-84	2644	—	1874	2763	2577	—	—	-626
CPU time		8200  s				32000  s	27000  s	8200  s					20000  s		9000  s						76000  s		19000  s	270  s				1600  s		22000  s			250  s					7300  s		11000  s		22000  s		3700  s						300  s		16000  s	83000  s	25000  s	66000  s		64000  s	90000  s	78000  s			5700  s
C.Termination 2146 valid tasks (1346 true, 800 false, 1 void), max. score: 3734		1607	—	2077	—	1332	1042	1085	—	—	—	—	1152	1358	—	—	—	—	0	—	796	—	1074	—	294	—	—	1614	—	-994	—	—	—	—	—	—	—	1571	356	860	—	985	—	878	—	3368	—	—	—	—	—	1427	796	583	2616	—	0	—	0	—	—	—
CPU time		13000  s		110000  s		12000  s	13000  s	5900  s					14000  s	110000  s							23000  s		5700  s		300  s			19000  s		59000  s								15000  s	8400  s	2300  s		44000  s		1900  s		80000  s						23000  s	23000  s	40000  s	62000  s
C.termination.BitVectors 34 valid tasks (23 true, 11 false, 0 void), max. score: 57		36	—	8	—	33	27	26	—	—	—	—	11	37	—	—	—	—	0	—	31	—	26	—	0	—	—	28	—	-115	—	—	—	—	—	—	—	10	-60	11	—	7	—	26	—	55	—	—	—	—	—	36	31	9	50	—	0	—	0	—	—	—
CPU time		5  s		36  s		66  s	110  s	4  s					47  s	560  s							3100  s		8  s					5  s		60  s								16  s	1  s	2  s		22  s		3  s		2700  s						36  s	3100  s	170  s	610  s
C.termination.MainControlFlow 281 valid tasks (220 true, 61 false, 0 void), max. score: 501		275	—	400	—	154	86	68	—	—	—	—	288	112	—	—	—	—	0	—	61	—	66	—	140	—	—	192	—	170	—	—	—	—	—	—	—	108	330	278	—	243	—	56	—	441	—	—	—	—	—	108	61	182	393	—	0	—	0	—	—	—
CPU time		120  s		2700  s		2400  s	1200  s	630  s					3000  s	4500  s							4200  s		1100  s		280  s			94  s		3100  s								570  s	3000  s	1900  s		2300  s		70  s		26000  s						1100  s	4200  s	5600  s	5200  s
C.termination.MainHeap 201 valid tasks (189 true, 12 false, 1 void), max. score: 390		0	—	286	—	36	26	24	—	—	—	—	5	0	—	—	—	—	0	—	0	—	22	—	0	—	—	150	—	0	—	—	—	—	—	—	—	258	196	5	—	0	—	24	—	352	—	—	—	—	—	24	0	0	168	—	0	—	0	—	—	—
CPU time				5000  s		65  s	82  s	12  s					32  s										9  s					15  s										1400  s	1100  s	1  s				2  s		23000  s						6  s			3400  s
C.termination.Other 1630 valid tasks (914 true, 716 false, 0 void), max. score: 2544		1562	—	1287	—	1281	1163	1460	—	—	—	—	1263	1701	—	—	—	—	0	—	578	—	1456	—	82	—	—	1230	—	1507	—	—	—	—	—	—	—	1576	454	432	—	1247	—	902	—	2184	—	—	—	—	—	1789	578	283	1910	—	0	—	0	—	—	—
CPU time		13000  s		100000  s		9000  s	12000  s	5200  s					11000  s	110000  s							15000  s		4600  s		25  s			19000  s		56000  s								13000  s	4300  s	370  s		41000  s		1800  s		29000  s						22000  s	16000  s	34000  s	52000  s
C.SoftwareSystems 4394 valid tasks (2860 true, 1534 false, 46 void), max. score: 7140		25	—	—	—	2121	1996	-1690	—	-1577	-3361	—	1496	—	—	—	—	—	-2524	—	-18	—	14	—	—	—	—	457	611	-362	—	—	-28819	—	—	—	—	2746	—	1477	—	-3112	—	—	—	—	—	—	—	—	-346	2614	-18	69	730	—	290	—	404	—	—	—
CPU time		58  s				94000  s	23000  s	6300  s		89000  s	89000  s		100000  s						10000  s		1800  s		31000  s					56000  s	60000  s	82000  s			1500  s					41000  s		86000  s		140000  s									3  s	22000  s	1800  s	1800  s	140000  s		86000  s		120000  s
C.no-overflow.SoftwareSystems-BusyBox 65 valid tasks (35 true, 30 false, 2 void), max. score: 100		0	—	—	—	0	0	0	—	0	0	—	4	—	-48	—	—	—	0	—	0	—	-64	0	—	—	—	4	4	0	—	—	-544	—	—	—	—	14	—	0	—	-16	—	—	—	—	—	—	—	0	0	0	0	0	0	—	0	—	0	—	—	—
CPU time													1200  s															3  s	2  s									530  s
C.no-overflow.SoftwareSystems-coreutils 29 valid tasks (29 true, 0 false, 2 void), max. score: 58		0	—	—	—	0	0	-112	—	0	0	—	0	—	0	—	—	—	0	—	0	—	4	0	—	—	—	0	0	0	—	—	-448	—	—	—	—	4	—	0	—	0	—	—	—	—	—	—	—	0	0	0	0	0	0	—	0	—	0	—	—	—
CPU time																							12  s															50  s
C.no-overflow.SoftwareSystems-uthash 27 valid tasks (27 true, 0 false, 0 void), max. score: 54		0	—	—	—	0	0	0	—	0	0	—	0	—	0	—	—	—	0	—	0	—	0	0	—	—	—	0	0	0	—	—	-80	—	—	—	—	50	—	0	—	0	—	—	—	—	—	—	—	0	0	38	0	0	2	—	0	—	0	—	—	—
CPU time																																						130  s														16  s			390  s
C.termination.SoftwareSystems-DeviceDriversLinux64 215 valid tasks (42 true, 173 false, 0 void), max. score: 257		7	—	—	—	54	48	-32	—	—	—	—	125	—	—	—	—	—	0	—	22	—	16	—	0	—	—	6	6	28	—	—	—	—	—	—	—	32	—	115	—	31	—	—	—	37	—	—	—	—	2	87	22	20	201	—	0	—	0	—	—	—
CPU time		2  s				61  s	53  s	100  s					1400  s								280  s		25  s					1  s	1  s	860  s								37  s		110  s		1100  s				63  s					0  s	130  s	280  s	390  s	11000  s
C.termination.SoftwareSystems-uthash 32 valid tasks (32 true, 0 false, 0 void), max. score: 64		0	—	—	—	50	42	38	—	—	—	—	0	—	—	—	—	—	0	—	0	—	0	—	0	—	—	0	0	0	—	—	—	—	—	—	—	36	—	0	—	0	—	—	—	54	—	—	—	—	0	50	0	0	0	—	0	—	0	—	—	—
CPU time						96  s	46  s	1300  s																														170  s								370  s						25  s
C.unreach-call.SoftwareSystems-AWS-C-Common 349 valid tasks (187 true, 162 false, 4 void), max. score: 536		-28	—	—	—	318	321	99	—	21	32	—	176	—	-431	—	—	—	-15	—	0	—	180	—	—	—	—	58	213	152	—	—	—	—	—	—	—	79	—	201	—	15	—	—	—	—	—	—	—	—	-74	260	0	0	120	—	29	—	61	—	—	—
CPU time		11  s				1600  s	4300  s	210  s		610  s	310  s		3300  s		210  s				570  s				1100  s					8  s	3600  s	6600  s			160  s					830  s		3300  s		2100  s									2  s	1900  s			8900  s		2500  s		7900  s
C.unreach-call.SoftwareSystems-DeviceDriversLinux64 2318 valid tasks (2122 true, 196 false, 22 void), max. score: 4440		290	—	—	—	575	527	-4843	—	3116	3112	—	2891	—	-21864	—	—	—	714	—	364	—	1608	—	—	—	—	3132	2676	2820	—	—	—	—	—	—	—	3456	—	2782	—	2671	—	—	—	—	—	—	—	—	-880	1328	364	364	2731	—	2171	—	2704	—	—	—
CPU time		44  s				90000  s	14000  s	87  s		85000  s	87000  s		76000  s		120  s				9000  s		1500  s		25000  s					56000  s	55000  s	72000  s			19  s					38000  s		62000  s		130000  s										9400  s	1500  s	1400  s	110000  s		84000  s		110000  s
C.unreach-call.SoftwareSystems-DeviceDriversLinux64Large 8 valid tasks (8 true, 0 false, 0 void), max. score: 16		0	—	—	—	0	0	0	—	2	2	—	4	—	-96	—	—	—	0	—	0	—	0	—	—	—	—	0	0	0	—	—	—	—	—	—	—	14	—	4	—	0	—	—	—	—	—	—	—	—	0	0	0	0	0	—	0	—	0	—	—	—
CPU time										380  s	330  s		280  s																									390  s		720  s
C.unreach-call.SoftwareSystems-Intel-TDX-Module 836 valid tasks (178 true, 658 false, 0 void), max. score: 1014		0	—	—	—	0	0	0	—	-2936	-3710	—	71	—	-2805	—	—	—	-7952	—	0	—	4	—	—	—	—	0	0	-382	—	—	-10269	—	—	—	—	0	—	64	—	-3702	—	—	—	—	—	—	—	—	0	0	0	0	0	—	0	—	0	—	—	—
CPU time										2600  s	670  s		14000  s		30  s				150  s				290  s							400  s			3  s							15000  s		1300  s
C.unreach-call.SoftwareSystems-Other 70 valid tasks (35 true, 35 false, 6 void), max. score: 105		0	—	—	—	33	22	-4	—	-272	-272	—	18	—	-12	—	—	—	4	—	0	—	35	—	—	—	—	0	22	-61	—	—	-364	—	—	—	—	22	—	27	—	17	—	—	—	—	—	—	—	—	0	33	0	0	8	—	2	—	8	—	—	—
CPU time						570  s	1200  s	770  s					730  s		3  s				260  s				67  s						1400  s	990  s			5  s					280  s		440  s		1000  s										1100  s			270  s		36  s		970  s
C.unreach-call.SoftwareSystems-uthash 32 valid tasks (32 true, 0 false, 0 void), max. score: 64		0	—	—	—	38	38	0	—	0	0	—	0	—	14	—	—	—	0	—	0	—	0	—	—	—	—	0	0	0	—	—	-480	—	—	—	—	32	—	0	—	0	—	—	—	—	—	—	—	—	0	32	0	0	0	—	0	—	0	—	—	—
CPU time						24  s	33  s								60  s																							110  s														9  s
C.valid-memcleanup.SoftwareSystems-uthash 27 valid tasks (15 true, 12 false, 0 void), max. score: 42		0	—	—	—	36	36	21	—	—	—	—	29	—	—	—	—	—	0	—	0	—	0	—	—	—	—	0	0	0	—	—	0	—	—	—	—	16	—	29	—	-137	—	—	—	—	—	—	—	8	0	36	0	0	0	—	0	—	0	—	—	—
CPU time						36  s	59  s	640  s			44  s		950  s																									53  s		1600  s		54  s								2  s		50  s
C.valid-memsafety.SoftwareSystems-coreutils 163 valid tasks (68 true, 95 false, 10 void), max. score: 231		0	—	—	—	2	2	-230	—	0	-265	—	6	—	—	—	—	—	0	—	0	—	-56	—	—	—	—	0	0	-411	—	—	-408	—	—	—	—	26	—	-26	—	-677	—	—	—	—	—	—	—	1	0	6	0	0	0	—	0	—	0	—	—	—
CPU time						0  s	1  s	2300  s			68  s		51  s										2900  s							350  s			19  s					180  s		15  s		130  s								5  s		52  s
C.valid-memsafety.SoftwareSystems-DeviceDriversLinux64 142 valid tasks (4 true, 138 false, 0 void), max. score: 146		2	—	—	—	92	91	10	—	0	54	—	41	—	—	—	—	—	0	—	0	—	12	—	—	—	—	8	8	9	—	—	—	—	—	—	—	8	—	36	—	38	—	—	—	—	—	—	—	1	-96	68	0	0	2	—	1	—	2	—	—	—
CPU time		1  s				1500  s	3200  s	100  s			640  s		2000  s										250  s					2  s	1  s	770  s			1300  s					7  s		1100  s		520  s								0  s		9200  s			110  s		49  s		160  s
C.valid-memsafety.SoftwareSystems-Other 49 valid tasks (31 true, 18 false, 0 void), max. score: 80		0	—	—	—	-9	-9	-78	—	0	0	—	0	—	—	—	—	—	0	—	-16	—	-31	—	—	—	—	0	0	0	—	—	-517	—	—	—	—	18	—	0	—	0	—	—	—	—	—	—	—	9	0	11	-16	0	0	—	0	—	0	—	—	—
CPU time						12  s	27  s	170  s															900  s										33  s					400  s												780  s		190  s
C.valid-memsafety.SoftwareSystems-uthash 32 valid tasks (15 true, 17 false, 0 void), max. score: 47		0	—	—	—	41	41	22	—	0	23	—	26	—	—	—	—	—	0	—	0	—	0	—	—	—	—	0	0	22	—	—	-466	—	—	—	—	18	—	30	—	23	—	—	—	—	—	—	—	13	0	41	0	0	0	—	0	—	0	—	—	—
CPU time						65  s	110  s	650  s			140  s		1500  s																	160  s			41  s					59  s		1700  s		160  s								4  s		220  s
C.FalseOverall 36402 valid tasks (24567 true, 11835 false, 121 void), max. score: 12195		3063	—	—	—	6362	6192	-2932	—	—	—	—	7389	—	—	—	—	—	476	—	1091	—	5232	—	—	—	—	—	—	-6603	—	—	—	—	—	—	—	1442	—	4089	—	2414	—	—	—	—	—	—	—	—	—	7833	-329	187	5835	—	3468	—	4243	—	—	—
CPU time		36000  s				68000  s	140000  s	140000  s					380000  s						140000  s		150000  s		95000  s							200000  s								25000  s		240000  s		200000  s										150000  s	150000  s	180000  s	190000  s		140000  s		190000  s
C.TrueOverall 36402 valid tasks (24567 true, 11835 false, 121 void), max. score: 48413		10883	—	—	—	13401	12083	13998	—	—	—	—	20589	—	—	—	—	—	242	—	10400	—	18732	—	—	—	—	22673	—	11090	—	—	—	—	—	—	—	20637	—	17538	—	12836	—	—	—	—	—	—	—	—	—	17638	11885	4178	25637	—	10347	—	17044	—	—	—
CPU time		120000  s				240000  s	120000  s	49000  s					490000  s						95000  s		750000  s		280000  s					86000  s		250000  s								93000  s		350000  s		940000  s										430000  s	410000  s	190000  s	730000  s		500000  s		690000  s
C.Overall 36402 valid tasks (24567 true, 11835 false, 121 void), max. score: 60609		13946	—	—	—	19763	18275	11066	—	—	—	—	27979	—	—	—	—	—	718	—	11491	—	23964	—	—	—	—	22673	—	4487	—	—	—	—	—	—	—	22079	—	21627	—	15249	—	—	—	—	—	—	—	—	—	25471	11556	4365	31472	—	13815	—	21287	—	—	—
CPU time		150000  s				310000  s	260000  s	190000  s					860000  s						230000  s		900000  s		380000  s					86000  s		450000  s								120000  s		590000  s		1100000  s										580000  s	570000  s	370000  s	920000  s		640000  s		880000  s
Participants	Plots	2LS	aise	AProVE (KoAT + LoAT)	BRICK	Bubaak	Bubaak-SpLit	CBMC	CoOpeRace	CPA-BAM-BnB	CPA-BAM-SMG	CPALockator	CPAchecker	CPV	Crux	CSeq	Dartagnan	Deagle	DIVINE	EBF	EmergenTheta	ESBMC-incr	ESBMC-kind	Frama-C-SV	ReFuncTion	Gazer-Theta	GDart-LLVM	Goblint	Goblitch	Graves-CPA	Hornix	iekke	Infer	Korn	Lazy-CSeq	LF-checker	Locksmith	Mopsa	MuVal	Nacpa	OGChecker	PeSCo-CPA	PIChecker	Pinaka	PredatorHP	PROTON	RacerF	Re3ver	SEAL	SV-sanitizers	SVF-SVC	Symbiotic	Theta	Thorn	UAutomizer	UGemCutter	UKojak	UParalizer	UTaipan	VeriAbs	VeriAbsL	VeriOover