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

Results of the Competition on Witness Validation

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

• Report of SV-COMP 2026 (Proc. TACAS 2026)
• The benchmarks and rules are also available from the competition web site.

The background color is gold for the winner, silver for the second, and bronze for the third.

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.
• 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. Validation of Correctness Witnesses v2
2. Validation of Violation Witnesses v2
3. Validation of Violation Witnesses v1

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. Validation of Correctness Witnesses v2

Ranking by Category (with Score-Based Quantile Plots)

C.ReachSafety 1. MetaVal 2. UAutomizer 3. CPAchecker	C.NoOverflows 1. UAutomizer 2. CPAchecker 3. Goblint	C.SoftwareSystems 1. Goblint 2. UAutomizer 3. CPAchecker
C.ValidationCrafted 1. Mopsa 2. Goblint 3. MetaVal
C.Overall 1. UAutomizer 2. CPAchecker 3. Goblint

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	CPAchecker	Goblint	LIV	MetaVal	Mopsa	Theta	UAutomizer	UGemCutter	UReferee
Representing Jury Member		Marian Lingsch-Rosenfeld	Simmo Saan	Marian Lingsch-Rosenfeld	Marian Lingsch-Rosenfeld	Raphaël Monat	Levente Bajczi	Marcel Ebbinghaus	Dominik Klumpp	Frank Schüssele
Affiliation		LMU Munich, Germany	University of Tartu, Estonia	LMU Munich, Germany	LMU Munich, Germany	Inria and University of Lille, France	Budapest University of Technology and Economics, Hungary	University of Freiburg, Germany	University of Freiburg, Germany	University of Freiburg, Germany
C.ReachSafety 42807 valid tasks (36864 correct, 5943 wrong, 22943 void), max. score: 64211		28910	13525	-14884	51786	-50037	0	35695	—	4403
CPU time		900000  s	31000  s	76000  s	1100000  s	130000  s		1100000  s		150000  s
C.unreach-call.BitVectors 357 valid tasks (306 correct, 51 wrong, 54 void), max. score: 536		201	155	-391	511	-9	0	439	—	57
CPU time		5300  s	680  s	670  s	8700  s	560  s		15000  s		890  s
C.unreach-call.Combinations 916 valid tasks (42 correct, 874 wrong, 641 void), max. score: 1374		414	0	0	1020	-436	0	726	—	0
CPU time		1500  s			22000  s			15000  s
C.unreach-call.ControlFlow 437 valid tasks (373 correct, 64 wrong, 107 void), max. score: 655		426	200	-271	499	207	0	478	—	164
CPU time		3100  s	3500  s	1200  s	4700  s	710  s		8800  s		2300  s
C.unreach-call.ECA 4859 valid tasks (3922 correct, 937 wrong, 1407 void), max. score: 7289		4786	279	-14802	3523	-74381	0	3311	—	0
CPU time		180000  s	3400  s	130  s	160000  s	5000  s		220000  s
C.unreach-call.Hardness 22751 valid tasks (21497 correct, 1254 wrong, 17125 void), max. score: 34126		22305	177	0	34047	1107	0	15344	—	1147
CPU time		540000  s	1900  s		600000  s	40000  s		390000  s		85000  s
C.unreach-call.Hardware 1179 valid tasks (689 correct, 490 wrong, 1160 void), max. score: 1769		411	544	0	1169	633	0	953	—	80
CPU time		3600  s	4400  s		14000  s	1300  s		55000  s		3200  s
C.unreach-call.Loops 5578 valid tasks (4917 correct, 661 wrong, 1689 void), max. score: 8367		1071	2861	-2538	6995	2117	0	6666	—	1738
CPU time		72000  s	9000  s	59000  s	130000  s	23000  s		170000  s		29000  s
C.unreach-call.ProductLines 4100 valid tasks (3562 correct, 538 wrong, 55 void), max. score: 6150		2072	2391	0	5507	3307	0	4049	—	679
CPU time		63000  s	7000  s		87000  s	59000  s		130000  s		32000  s
C.unreach-call.Recursive 760 valid tasks (633 correct, 127 wrong, 228 void), max. score: 1140		135	695	6	898	513	0	895	—	0
CPU time		1600  s	1100  s	470  s	9500  s	2200  s		40000  s
C.unreach-call.Sequentialized 1175 valid tasks (356 correct, 819 wrong, 446 void), max. score: 1763		1033	53	0	1473	37	0	232	—	0
CPU time		18000  s	11  s		56000  s	190  s		9600  s
C.unreach-call.XCSP 695 valid tasks (567 correct, 128 wrong, 31 void), max. score: 1043		953	0	961	956	0	0	233	—	0
CPU time		13000  s		15000  s	15000  s			7300  s
C.Concurrency 4872 valid tasks (4749 correct, 123 wrong, 889 void), max. score: 7308		—	764 Demo	—	—	0 Demo	0 Demo	7291 Demo	7308 Demo	—
CPU time			190  s					190000  s	200000  s
C.no-overflow.Concurrency 3533 valid tasks (3468 correct, 65 wrong, 578 void), max. score: 5300		—	356 Demo	—	—	0 Demo	0 Demo	5286 Demo	5300 Demo	—
CPU time			130  s					150000  s	160000  s
C.unreach-call.Concurrency 1339 valid tasks (1281 correct, 58 wrong, 311 void), max. score: 2009		—	285 Demo	—	—	0 Demo	0 Demo	2004 Demo	2009 Demo	—
CPU time			53  s					48000  s	38000  s
C.NoOverflows 47221 valid tasks (39602 correct, 7619 wrong, 3637 void), max. score: 70832		54068	39671	0	0	-22315	0	63546	—	0
CPU time		390000  s	8700  s			67000  s		1400000  s
C.no-overflow.Juliet 35040 valid tasks (28708 correct, 6332 wrong, 1667 void), max. score: 52560		39599	32423	0	0	-57513	0	46243	—	0
CPU time		260000  s	4900  s			44000  s		960000  s
C.no-overflow.Main 12181 valid tasks (10894 correct, 1287 wrong, 1970 void), max. score: 18272		14129	9196	0	0	8481	0	16709	—	0
CPU time		130000  s	3800  s			22000  s		400000  s
C.Termination 6469 valid tasks (4885 correct, 1584 wrong, 2831 void), max. score: 9704		-2804 Demo	5303 Demo	—	1485 Demo	-1504 Demo	—	—	—	—
CPU time		12000  s	39000  s		73000  s	51000  s
C.termination.BitVectors 61 valid tasks (39 correct, 22 wrong, 79 void), max. score: 92		13 Demo	58 Demo	—	61 Demo	45 Demo	—	—	—	—
CPU time		43  s	18  s		1900  s	69  s
C.termination.MainControlFlow 435 valid tasks (312 correct, 123 wrong, 832 void), max. score: 653		-416 Demo	258 Demo	—	-215 Demo	396 Demo	—	—	—	—
CPU time		370  s	42  s		13000  s	2600  s
C.termination.MainHeap 226 valid tasks (202 correct, 24 wrong, 432 void), max. score: 339		-292 Demo	226 Demo	—	0 Demo	217 Demo	—	—	—	—
CPU time		45  s	56  s			3100  s
C.termination.Other 5747 valid tasks (4332 correct, 1415 wrong, 1488 void), max. score: 8621		1785 Demo	4236 Demo	—	2371 Demo	-20369 Demo	—	—	—	—
CPU time		11000  s	39000  s		59000  s	45000  s
C.SoftwareSystems 15708 valid tasks (13619 correct, 2089 wrong, 3868 void), max. score: 21991		4314	9411	0	0	3772	0	7706	—	2759
CPU time		73000  s	90000  s			110000  s		490000  s		110000  s
C.no-overflow.SoftwareSystems-BusyBox 63 valid tasks (3 correct, 60 wrong, 86 void), max. score: 95		0	63	0	0	13	0	0	—	0
CPU time			5  s			4  s
C.termination.SoftwareSystems-DeviceDriversLinux64 360 valid tasks (18 correct, 342 wrong, 133 void), max. score: 540		0 Demo	360 Demo	0 Demo	0 Demo	360 Demo	12 Demo	0 Demo	—	0 Demo
CPU time			9  s			27  s	330  s
C.unreach-call.SoftwareSystems-AWS-C-Common 681 valid tasks (355 correct, 326 wrong, 650 void), max. score: 1022		512	441	0	0	537	0	652	—	183
CPU time		6100  s	75  s			1400  s		24000  s		3900  s
C.unreach-call.SoftwareSystems-DeviceDriversLinux64 13600 valid tasks (13244 correct, 356 wrong, 2674 void), max. score: 20400		5182	11927	0	0	12595	0	13918	—	4299
CPU time		66000  s	90000  s			110000  s		470000  s		100000  s
C.unreach-call.SoftwareSystems-Intel-TDX-Module 1291 valid tasks (0 correct, 1291 wrong, 373 void), max. score: 1291		6	0	0	0	0	0	0	—	0
CPU time		360  s
C.unreach-call.SoftwareSystems-Other 73 valid tasks (17 correct, 56 wrong, 85 void), max. score: 110		17	34	0	0	-52	0	35	—	21
CPU time		180  s	610  s			190  s		1400  s		100  s
C.ValidationCrafted 18 valid tasks (15 correct, 3 wrong, 0 void), max. score: 27		11	13	-38	13	14	0	13	—	7
CPU time		86  s	3  s		250  s	28  s		440  s		94  s
C.unreach-call.CorrectnessWitnesses 18 valid tasks (15 correct, 3 wrong, 0 void), max. score: 27		11	13	-38	13	14	0	13	—	7
CPU time		86  s	3  s		250  s	28  s		440  s		94  s
C.Overall 105754 valid tasks (90100 correct, 15654 wrong, 30448 void), max. score: 155987		71251	65792	-65595	51372	-15899	0	89983	—	17938
CPU time		1400000  s	130000  s	76000  s	1100000  s	310000  s		2900000  s		260000  s
Participants	Plots	CPAchecker	Goblint	LIV	MetaVal	Mopsa	Theta	UAutomizer	UGemCutter	UReferee

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.

2. Validation of Violation Witnesses v2

Ranking by Category (with Score-Based Quantile Plots)

C.ReachSafety 1. CPAchecker 2. Witch 3. UAutomizer	C.MemSafety 1. UAutomizer 2. Witch 3. CPAchecker	C.NoOverflows 1. UAutomizer 2. CPAchecker 3. Witch
C.Termination 1. Witch 2. CPAchecker 3. UAutomizer	C.SoftwareSystems 1. Witch 2. UAutomizer 3. CPAchecker	C.ValidationCrafted 1. Witch 2. Theta 3. -
C.Overall 1. Witch 2. CPAchecker 3. Theta

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	CPAchecker	MetaVal	Theta	UAutomizer	Witch
Representing Jury Member		Marian Lingsch-Rosenfeld	Marian Lingsch-Rosenfeld	Levente Bajczi	Marcel Ebbinghaus	Paulína Ayaziová
Affiliation		LMU Munich, Germany	LMU Munich, Germany	Budapest University of Technology and Economics, Hungary	University of Freiburg, Germany	Masaryk University, Brno, Czechia
C.ReachSafety 19560 valid tasks (5819 correct, 13741 wrong, 6142 void), max. score: 30039		16829	1298	0	8477	16204
CPU time		180000  s	300000  s		250000  s	43000  s
C.unreach-call.Arrays 796 valid tasks (530 correct, 266 wrong, 304 void), max. score: 1194		773	291	0	420	309
CPU time		3600  s	9000  s		9700  s	460  s
C.unreach-call.BitVectors 128 valid tasks (98 correct, 30 wrong, 42 void), max. score: 192		158	1	0	66	150
CPU time		760  s	2000  s		2900  s	440  s
C.unreach-call.Combinations 1212 valid tasks (751 correct, 461 wrong, 814 void), max. score: 1818		687	328	0	735	1011
CPU time		25000  s	13000  s		26000  s	5300  s
C.unreach-call.ControlFlow 122 valid tasks (89 correct, 33 wrong, 49 void), max. score: 183		-104	119	0	176	94
CPU time		440  s	1600  s		2400  s	230  s
C.unreach-call.ECA 1397 valid tasks (405 correct, 992 wrong, 1413 void), max. score: 2096		1947	21	0	99	1923
CPU time		35000  s	580  s		6700  s	9800  s
C.unreach-call.Floats 1224 valid tasks (160 correct, 1064 wrong, 430 void), max. score: 1836		1467	494	0	1477	-242
CPU time		14000  s	3300  s		36000  s	81  s
C.unreach-call.Hardness 9397 valid tasks (0 correct, 9397 wrong, 0 void), max. score: 18794		8326	7818	0	5250	1282
CPU time		46000  s	200000  s		65000  s	4100  s
C.unreach-call.Hardware 802 valid tasks (334 correct, 468 wrong, 545 void), max. score: 1203		1098	-227	0	-786	1171
CPU time		12000  s	7800  s		4900  s	5000  s
C.unreach-call.Heap 406 valid tasks (308 correct, 98 wrong, 260 void), max. score: 609		255	-243	0	77	349
CPU time		2300  s	4300  s		7000  s	490  s
C.unreach-call.Loops 924 valid tasks (657 correct, 267 wrong, 860 void), max. score: 1386		458	-835	0	863	979
CPU time		6300  s	12000  s		19000  s	2500  s
C.unreach-call.ProductLines 1065 valid tasks (977 correct, 88 wrong, 479 void), max. score: 1598		506	1351	0	460	-1
CPU time		6500  s	34000  s		26000  s	3300  s
C.unreach-call.Recursive 377 valid tasks (350 correct, 27 wrong, 184 void), max. score: 566		346	-893	0	100	391
CPU time		3600  s	5200  s		6000  s	740  s
C.unreach-call.Sequentialized 1386 valid tasks (893 correct, 493 wrong, 531 void), max. score: 2079		1944	96	0	145	1954
CPU time		20000  s	4200  s		33000  s	3600  s
C.unreach-call.XCSP 324 valid tasks (267 correct, 57 wrong, 231 void), max. score: 486		441	281	0	62	419
CPU time		5400  s	5000  s		5000  s	6500  s
C.MemSafety 655 valid tasks (644 correct, 11 wrong, 1968 void), max. score: 901		632	0	0	832	791
CPU time		4300  s			17000  s	1800  s
C.valid-memsafety.Arrays 6 valid tasks (3 correct, 3 wrong, 43 void), max. score: 9		8	0	0	9	5
CPU time		27  s			100  s	5  s
C.valid-memsafety.Heap 53 valid tasks (46 correct, 7 wrong, 104 void), max. score: 79		72	0	0	74	79
CPU time		330  s			880  s	43  s
C.valid-memsafety.Juliet 592 valid tasks (592 correct, 0 wrong, 1804 void), max. score: 592		592	0	0	506	592
CPU time		4000  s			16000  s	1700  s
C.valid-memsafety.Other 4 valid tasks (3 correct, 1 wrong, 17 void), max. score: 6		1	0	0	5	6
CPU time		12  s			74  s	5  s
C.NoOverflows 9664 valid tasks (9496 correct, 168 wrong, 11259 void), max. score: 12080		9961	0	0	11196	9147
CPU time		73000  s			200000  s	32000  s
C.no-overflow.Juliet 7519 valid tasks (7519 correct, 0 wrong, 9435 void), max. score: 7519		7519	0	0	7519	7330
CPU time		61000  s			160000  s	24000  s
C.no-overflow.Main 2145 valid tasks (1977 correct, 168 wrong, 1824 void), max. score: 3218		2277	0	0	2825	1969
CPU time		11000  s			41000  s	8400  s
C.Termination 1483 valid tasks (1483 correct, 0 wrong, 303 void), max. score: 1483		1348	0	832	1238	1359
CPU time		43000  s		9100  s	48000  s	1400  s
C.termination.BitVectors 51 valid tasks (51 correct, 0 wrong, 1 void), max. score: 51		50	0	40	30	49
CPU time		720  s		410  s	490  s	36  s
C.termination.MainControlFlow 186 valid tasks (186 correct, 0 wrong, 6 void), max. score: 186		179	0	125	174	172
CPU time		2300  s		1400  s	3600  s	150  s
C.termination.Other 1246 valid tasks (1246 correct, 0 wrong, 296 void), max. score: 1246		976	0	283	1222	1077
CPU time		40000  s		7300  s	44000  s	1200  s
C.SoftwareSystems 824 valid tasks (332 correct, 492 wrong, 2081 void), max. score: 1288		524	0	83	566	759
CPU time		7500  s		1400  s	11000  s	2200  s
C.termination.SoftwareSystems-DeviceDriversLinux64 107 valid tasks (107 correct, 0 wrong, 0 void), max. score: 107		104	0	86	104	107
CPU time		870  s		1400  s	2900  s	120  s
C.unreach-call.SoftwareSystems-AWS-C-Common 290 valid tasks (160 correct, 130 wrong, 556 void), max. score: 435		267	0	0	177	315
CPU time		3300  s			4300  s	1700  s
C.unreach-call.SoftwareSystems-DeviceDriversLinux64 139 valid tasks (14 correct, 125 wrong, 414 void), max. score: 209		109	0	0	98	52
CPU time		1900  s			3100  s	160  s
C.unreach-call.SoftwareSystems-Intel-TDX-Module 174 valid tasks (0 correct, 174 wrong, 910 void), max. score: 348		34	0	0	0	0
CPU time		500  s
C.unreach-call.SoftwareSystems-Other 37 valid tasks (6 correct, 31 wrong, 138 void), max. score: 56		40	0	0	45	44
CPU time		190  s			710  s	69  s
C.unreach-call.SoftwareSystems-uthash 30 valid tasks (0 correct, 30 wrong, 0 void), max. score: 60		4	0	0	0	22
CPU time		30  s				11  s
C.valid-memsafety.SoftwareSystems-DeviceDriversLinux64 45 valid tasks (45 correct, 0 wrong, 56 void), max. score: 45		45	0	0	0	45
CPU time		760  s				220  s
C.valid-memsafety.SoftwareSystems-Other 2 valid tasks (0 correct, 2 wrong, 7 void), max. score: 4		0	0	0	4	4
CPU time					89  s	5  s
C.ValidationCrafted 117 valid tasks (49 correct, 68 wrong, 0 void), max. score: 176		-113	-340	24	-492	163
CPU time		410  s	450  s	48  s	1100  s	150  s
C.unreach-call.ViolationWitnesses 100 valid tasks (41 correct, 59 wrong, 0 void), max. score: 150		68	-581	0	-599	150
CPU time		250  s	450  s		1000  s	140  s
C.termination.ViolationWitnesses 17 valid tasks (8 correct, 9 wrong, 0 void), max. score: 26		-44	0	7	-41	22
CPU time		150  s		48  s	73  s	10  s
C.Overall 32303 valid tasks (17823 correct, 14480 wrong, 21753 void), max. score: 44272		18482	-15295	4665	972	33434
CPU time		310000  s	300000  s	10000  s	530000  s	81000  s
Participants	Plots	CPAchecker	MetaVal	Theta	UAutomizer	Witch

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.

3. Validation of Violation Witnesses v1

Ranking by Category (with Score-Based Quantile Plots)

C.ReachSafety 1. ConcurrentWitness2Test 2. - 3. -	C.MemSafety 1. CPAchecker 2. - 3. -	C.Concurrency 1. Dartagnan 2. UAutomizer 3. CPAchecker
C.Termination 1. UAutomizer 2. - 3. -	C.SoftwareSystems 1. CPAchecker 2. UAutomizer 3. -

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	ConcurrentWitness2Test	CPA-witness2test	CPAchecker	Dartagnan	CProver-witness2test	MetaVal	NITWIT	Symbiotic-Witch	UAutomizer
Representing Jury Member		Zsófia Ádám	inactive	Marian Lingsch-Rosenfeld	Hernán Ponce de León	inactive	inactive	inactive	inactive	Marcel Ebbinghaus
Affiliation		Budapest University of Technology and Economics, Hungary		LMU Munich, Germany	Huawei Dresden Research Center, Germany					University of Freiburg, Germany
C.ReachSafety 35069 valid tasks (18168 correct, 16901 wrong, 13554 void), max. score: 53856		3389	9840	-16228	—	-10564	-33601	9034	10626	-138972
CPU time		6100  s	120000  s	300000  s		46000  s	260000  s	11000  s	100000  s	630000  s
C.unreach-call.Arrays 1571 valid tasks (731 correct, 840 wrong, 990 void), max. score: 2357		49	874	-1443	—	-2520	50	720	833	-9909
CPU time		140  s	4100  s	4300  s		1200  s	7800  s	3400  s	2100  s	20000  s
C.unreach-call.BitVectors 315 valid tasks (212 correct, 103 wrong, 62 void), max. score: 473		61	164	-103	—	19	137	123	131	-689
CPU time		31  s	1100  s	2100  s		250  s	3000  s	3  s	1300  s	5800  s
C.unreach-call.Combinations 3063 valid tasks (1746 correct, 1317 wrong, 2005 void), max. score: 4595		0	638	29	—	-1236	499	-280	845	-16665
CPU time			14000  s	41000  s		7200  s	13000  s	96  s	5800  s	75000  s
C.unreach-call.ControlFlow 333 valid tasks (178 correct, 155 wrong, 170 void), max. score: 500		123	-47	4	—	107	-1542	27	-257	-188
CPU time		54  s	430  s	1300  s		260  s	2100  s	0  s	590  s	4600  s
C.unreach-call.ECA 4936 valid tasks (3734 correct, 1202 wrong, 1513 void), max. score: 7404		5	1759	3371	—	-4259	57	2312	1643	-36744
CPU time		20  s	56000  s	79000  s		24000  s	2300  s	6100  s	26000  s	83000  s
C.unreach-call.Floats 2651 valid tasks (588 correct, 2063 wrong, 1173 void), max. score: 3977		242	824	-3514	—	-4650	-748	714	878	-3242
CPU time		61  s	3400  s	10000  s		1600  s	24000  s	5  s	320  s	66000  s
C.unreach-call.Hardness 6877 valid tasks (0 correct, 6877 wrong, 0 void), max. score: 13754		-16	-32	1210	—	-26	3994	0	138	13748
CPU time				6600  s		3  s	66000  s		970  s	120000  s
C.unreach-call.Hardware 1489 valid tasks (815 correct, 674 wrong, 2458 void), max. score: 2234		196	245	1193	—	260	0	0	581	-8324
CPU time		1800  s	5600  s	27000  s		760  s			4100  s	26000  s
C.unreach-call.Heap 1266 valid tasks (952 correct, 314 wrong, 330 void), max. score: 1899		29	683	-1674	—	-681	-619	318	238	-3168
CPU time		230  s	3600  s	7400  s		1100  s	11000  s	6  s	890  s	19000  s
C.unreach-call.Loops 3534 valid tasks (2020 correct, 1514 wrong, 1354 void), max. score: 5301		553	1649	-5631	—	-817	1449	1161	2283	-16875
CPU time		2200  s	9000  s	19000  s		2700  s	26000  s	24  s	7500  s	49000  s
C.unreach-call.ProductLines 4080 valid tasks (3206 correct, 874 wrong, 1222 void), max. score: 6120		80	0	-8152	—	313	2995	1484	1202	-23613
CPU time		1200  s		38000  s		4100  s	46000  s	58  s	26000  s	65000  s
C.unreach-call.Recursive 783 valid tasks (433 correct, 350 wrong, 674 void), max. score: 1175		253	427	-1441	—	11	-8779	233	97	-4350
CPU time		280  s	2300  s	5600  s		960  s	6400  s	160  s	390  s	12000  s
C.unreach-call.Sequentialized 3319 valid tasks (2834 correct, 485 wrong, 1268 void), max. score: 4979		35	1223	-807	—	613	864	1525	1745	-15750
CPU time		48  s	22000  s	44000  s		1200  s	36000  s	970  s	10000  s	60000  s
C.unreach-call.XCSP 852 valid tasks (719 correct, 133 wrong, 335 void), max. score: 1278		3	31	1201	—	297	490	281	802	-4563
CPU time		2  s	810  s	17000  s		720  s	19000  s	21  s	16000  s	21000  s
C.MemSafety 9390 valid tasks (7641 correct, 1749 wrong, 18084 void), max. score: 14085		—	-1616	6653	—	-1434	0	—	-10085	-17356
CPU time			3600  s	69000  s		1400  s			13000  s	170000  s
C.valid-memcleanup.Main 382 valid tasks (334 correct, 48 wrong, 396 void), max. score: 573		—	0	524	—	-379	0	—	69	341
CPU time				2800  s		45  s			210  s	9400  s
C.valid-memsafety.Arrays 257 valid tasks (255 correct, 2 wrong, 133 void), max. score: 386		—	32	-149	—	-207	0	—	241	-1043
CPU time			470  s	1200  s		190  s			250  s	4400  s
C.valid-memsafety.Heap 980 valid tasks (845 correct, 135 wrong, 884 void), max. score: 1470		—	-482	-103	—	-927	0	—	-934	-4616
CPU time			2800  s	6400  s		980  s			1100  s	9000  s
C.valid-memsafety.Juliet 7569 valid tasks (6022 correct, 1547 wrong, 16408 void), max. score: 11354		—	0	11334	—	0	0	—	-2152	8429
CPU time				57000  s					11000  s	150000  s
C.valid-memsafety.LinkedLists 141 valid tasks (130 correct, 11 wrong, 194 void), max. score: 212		—	-101	211	—	201	0	—	-1099	-686
CPU time			320  s	1100  s		150  s			68  s	620  s
C.valid-memsafety.Other 61 valid tasks (55 correct, 6 wrong, 69 void), max. score: 92		—	3	35	—	25	0	—	90	33
CPU time			42  s	360  s		30  s			130  s	820  s
C.Concurrency 3799 valid tasks (695 correct, 3104 wrong, 7529 void), max. score: 5699		—	—	1487	3299	—	—	—	—	3199
CPU time				13000  s	28000  s					82000  s
C.no-data-race.Concurrency 804 valid tasks (149 correct, 655 wrong, 2001 void), max. score: 1206		—	—	293	891	—	—	—	—	869
CPU time				3500  s	7000  s					14000  s
C.no-overflow.Concurrency 1647 valid tasks (23 correct, 1624 wrong, 63 void), max. score: 2471		—	—	0	1139	—	—	—	—	2366
CPU time					6500  s					38000  s
C.unreach-call.Concurrency 1315 valid tasks (493 correct, 822 wrong, 5242 void), max. score: 1973		21	—	46	1106	—	—	—	—	-195
CPU time		71  s		9100  s	14000  s					30000  s
C.valid-memsafety.Concurrency 33 valid tasks (30 correct, 3 wrong, 223 void), max. score: 50		—	—	39	28	—	—	—	—	33
CPU time				490  s	830  s					61  s
C.NoOverflows 24250 valid tasks (15418 correct, 8832 wrong, 26267 void), max. score: 36375		—	16165	-13368	—	-33601	0	—	1048	-9733
CPU time			120000  s	300000  s		25000  s			54000  s	470000  s
C.no-overflow.Juliet 17019 valid tasks (9733 correct, 7286 wrong, 24646 void), max. score: 25529		—	20176	-23351	—	10098	0	—	-11831	-8855
CPU time			110000  s	250000  s		20000  s			26000  s	350000  s
C.no-overflow.Main 7231 valid tasks (5685 correct, 1546 wrong, 1621 void), max. score: 10847		—	1068	1949	—	-24329	0	—	5652	-2042
CPU time			14000  s	45000  s		4600  s			29000  s	120000  s
C.Termination 1685 valid tasks (1651 correct, 34 wrong, 4626 void), max. score: 2528		—	—	-3861	—	—	0	—	—	1211
CPU time				42000  s						43000  s
C.termination.BitVectors 46 valid tasks (34 correct, 12 wrong, 46 void), max. score: 69		—	—	-188	—	—	0	—	—	54
CPU time				980  s						750  s
C.termination.MainControlFlow 236 valid tasks (224 correct, 12 wrong, 303 void), max. score: 354		—	—	-1436	—	—	0	—	—	138
CPU time				2500  s						4600  s
C.termination.MainHeap 10 valid tasks (8 correct, 2 wrong, 36 void), max. score: 15		—	—	5	—	—	0	—	—	5
CPU time				83  s						150  s
C.termination.Other 1393 valid tasks (1385 correct, 8 wrong, 4241 void), max. score: 2090		—	—	697	—	—	0	—	—	871
CPU time				39000  s						38000  s
C.SoftwareSystems 7003 valid tasks (1069 correct, 5934 wrong, 5794 void), max. score: 12255		—	1257	3893	—	-1663	363	0	2525	1795
CPU time			2000  s	58000  s		1600  s	51000  s		2900  s	160000  s
C.no-overflow.SoftwareSystems-BusyBox 43 valid tasks (0 correct, 43 wrong, 52 void), max. score: 86		—	0	6	—	0	0	0	0	76
CPU time				100  s						1200  s
C.no-overflow.SoftwareSystems-coreutils 93 valid tasks (0 correct, 93 wrong, 14 void), max. score: 186		—	0	0	—	0	0	0	0	0
CPU time
C.no-overflow.SoftwareSystems-uthash 42 valid tasks (0 correct, 42 wrong, 0 void), max. score: 84		—	56	0	—	0	0	0	72	84
CPU time			260  s						39  s	1000  s
C.termination.SoftwareSystems-DeviceDriversLinux64 180 valid tasks (171 correct, 9 wrong, 477 void), max. score: 270		—	0	170	—	0	0	0	0	270
CPU time				2300  s						5200  s
C.unreach-call.SoftwareSystems-AWS-C-Common 1135 valid tasks (547 correct, 588 wrong, 1095 void), max. score: 1703		—	0	323	—	356	511	0	711	-9877
CPU time				13000  s		970  s	16000  s		2700  s	19000  s
C.unreach-call.SoftwareSystems-DeviceDriversLinux64 4550 valid tasks (140 correct, 4410 wrong, 835 void), max. score: 6825		—	4	4016	—	429	3505	0	5	5243
CPU time			33  s	38000  s		510  s	32000  s		8  s	130000  s
C.unreach-call.SoftwareSystems-DeviceDriversLinux64Large 14 valid tasks (0 correct, 14 wrong, 0 void), max. score: 28		—	0	0	—	0	0	0	0	0
CPU time
C.unreach-call.SoftwareSystems-Intel-TDX-Module 459 valid tasks (0 correct, 459 wrong, 1838 void), max. score: 918		—	0	0	—	0	32	0	0	0
CPU time							440  s
C.unreach-call.SoftwareSystems-Other 244 valid tasks (59 correct, 185 wrong, 222 void), max. score: 366		—	0	-6	—	-1407	-292	0	-119	-49
CPU time				2500  s		130  s	1800  s		69  s	3200  s
C.unreach-call.SoftwareSystems-uthash 73 valid tasks (0 correct, 73 wrong, 0 void), max. score: 146		—	0	4	—	0	46	0	68	146
CPU time				96  s			690  s		32  s	1700  s
C.valid-memcleanup.SoftwareSystems-uthash 11 valid tasks (8 correct, 3 wrong, 82 void), max. score: 17		—	0	16	—	0	0	0	16	0
CPU time				250  s					11  s
C.valid-memsafety.SoftwareSystems-DeviceDriversLinux64 144 valid tasks (134 correct, 10 wrong, 960 void), max. score: 216		—	62	216	—	5	0	0	2	154
CPU time			1700  s	1700  s		15  s			5  s	1100  s
C.valid-memsafety.SoftwareSystems-Other 1 valid tasks (0 correct, 1 wrong, 72 void), max. score: 2		—	0	2	—	2	0	0	0	2
CPU time				11  s		2  s				65  s
C.valid-memsafety.SoftwareSystems-uthash 14 valid tasks (10 correct, 4 wrong, 147 void), max. score: 21		—	11	7	—	0	0	0	11	14
CPU time			54  s	170  s					13  s	170  s
C.Overall 81196 valid tasks (44642 correct, 36554 wrong, 75854 void), max. score: 125660		—	—	-22325	—	—	-14030	—	—	-59481
CPU time				780000  s			310000  s			1600000  s
Participants	Plots	ConcurrentWitness2Test	CPA-witness2test	CPAchecker	Dartagnan	CProver-witness2test	MetaVal	NITWIT	Symbiotic-Witch	UAutomizer

If you did not find what you are looking for, please do not hesitate to contact Dirk Beyer (competition webmaster).