TACAS 2025
14th Competition on Software Verification (SV-COMP 2025)

Results of the Competition on Witness Validation

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

• Report of SV-COMP 2025 (Proc. TACAS 2025)
• 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 2025 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.

Contents

1. Validation of Correctness Witnesses (Version 2.0)
2. Validation of Violation Witnesses (Version 2.0)
3. Validation of Correctness Witnesses (Version 1.0)
4. Validation of Violation Witnesses (Version 1.0)

1. Validation of Correctness Witnesses (Version 2.0)

Ranking by Category (with Score-Based Quantile Plots)

ReachSafety 1. UAutomizer 2. CPAchecker 3. LIV	NoOverflows 1. UAutomizer 2. CPAchecker 3. Mopsa	SoftwareSystems 1. Mopsa 2. CPAchecker 3. MetaVal
ValidationCrafted 1. UAutomizer 2. CPAchecker 3. –	Overall 1. UAutomizer 2. CPAchecker 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	CPAchecker	Goblint	LIV	MetaVal	MetaVal++	Mopsa	UAutomizer	UReferee
Representing Jury Member		Marian Lingsch-Rosenfeld	Simmo Saan	Marian Lingsch-Rosenfeld	Marian Lingsch-Rosenfeld	Marian Lingsch-Rosenfeld	Raphaël Monat	Marcel Ebbinghaus	Frank Schüssele
Affiliation		LMU Munich, Germany	University of Tartu, Estonia	LMU Munich, Germany	LMU Munich, Germany	LMU Munich, Germany	Inria and University of Lille, France	University of Freiburg, Germany	University of Freiburg, Germany
ReachSafety 19365 valid tasks (17373 correct, 1992 wrong, 11897 void), max. score: 28241		10378	3994	6829	-32688	-1164	6444	16085	2601
CPU time		660000 s	1300 s	180000 s	650000 s	9300 s	200000 s	720000 s	80000 s
ReachSafety-BitVectors 185 valid tasks (169 correct, 16 wrong, 83 void), max. score: 278		-50	67	76	80	49	81	229	90
CPU time		3800 s	6.6 s	250 s	8500 s	290 s	350 s	12000 s	1600 s
ReachSafety-ControlFlow 190 valid tasks (143 correct, 47 wrong, 68 void), max. score: 285		170	23	32	-1119	-283	60	163	77
CPU time		1200 s	2.3 s	140 s	1200 s	7000 s	3200 s	3800 s	6200 s
ReachSafety-ECA 1809 valid tasks (1424 correct, 385 wrong, 2070 void), max. score: 2714		1739	23	1790	11	4	13	1637	0
CPU time		59000 s	68 s	59000 s	1400 s	34 s	48 s	110000 s	0 s
ReachSafety-Loops 2683 valid tasks (2476 correct, 207 wrong, 1066 void), max. score: 4024		1070	679	688	1191	622	1526	3099	1169
CPU time		40000 s	180 s	7000 s	92000 s	890 s	17000 s	120000 s	20000 s
ReachSafety-ProductLines 1712 valid tasks (1445 correct, 267 wrong, 1107 void), max. score: 2568		684	735	0	540	0	1712	1688	140
CPU time		24000 s	230 s	0 s	89000 s	0 s	99000 s	69000 s	5500 s
ReachSafety-Recursive 306 valid tasks (255 correct, 51 wrong, 276 void), max. score: 459		40	272	78	-716	0	214	287	0
CPU time		160 s	43 s	340 s	1400 s	0 s	1700 s	30000 s	0 s
ReachSafety-Sequentialized 471 valid tasks (71 correct, 400 wrong, 690 void), max. score: 706		332	46	-149	345	0	80	174	13
CPU time		4800 s	2.4 s	170 s	15000 s	0 s	24 s	12000 s	70 s
ReachSafety-XCSP 385 valid tasks (316 correct, 69 wrong, 118 void), max. score: 578		519	0	385	261	0	0	39	0
CPU time		9200 s	0 s	27000 s	7400 s	0 s	0 s	1600 s	0 s
ReachSafety-Combinations 456 valid tasks (26 correct, 430 wrong, 645 void), max. score: 684		35	0	0	456	0	0	465	0
CPU time		740 s	0 s	0 s	7300 s	0 s	0 s	18000 s	0 s
ReachSafety-Hardware 428 valid tasks (313 correct, 115 wrong, 767 void), max. score: 642		130	133	232	0	115	298	387	55
CPU time		1200 s	780 s	1100 s	0 s	1100 s	2400 s	30000 s	2700 s
ReachSafety-Hardness 10738 valid tasks (10735 correct, 3 wrong, 5006 void), max. score: 16107		10595	15	9959	3922	0	1089	5285	511
CPU time		520000 s	2.8 s	84000 s	420000 s	0 s	71000 s	310000 s	43000 s
ReachSafety-Fuzzle 2 valid tasks (0 correct, 2 wrong, 1 void), max. score: 2		1	0	0	-32	0	0	2	0
CPU time		260 s	0 s	0 s	0 s	0 s	0 s	290 s	0 s
NoOverflows 26686 valid tasks (22175 correct, 4511 wrong, 8847 void), max. score: 40029		26940	18334	-4162	0	0	25022	32637	0
CPU time		210000 s	3100 s	19000 s	0 s	0 s	43000 s	970000 s	0 s
NoOverflows-Main 6571 valid tasks (5974 correct, 597 wrong, 3190 void), max. score: 9856		6274	3465	-2050	0	0	5752	7735	0
CPU time		71000 s	690 s	19000 s	0 s	0 s	18000 s	300000 s	0 s
NoOverflows-Juliet 20115 valid tasks (16201 correct, 3914 wrong, 5657 void), max. score: 30172		21406	17032	0	0	0	20115	25523	0
CPU time		140000 s	2400 s	0 s	0 s	0 s	26000 s	670000 s	0 s
SoftwareSystems 7581 valid tasks (7139 correct, 442 wrong, 7123 void), max. score: 11913		5092	2103	0	3182	0	7751	1951	954
CPU time		43000 s	120000 s	0 s	220000 s	0 s	100000 s	410000 s	82000 s
SoftwareSystems-AWS-C-Common-ReachSafety 371 valid tasks (201 correct, 170 wrong, 332 void), max. score: 556		345	168	0	185	0	229	227	74
CPU time		12000 s	28 s	0 s	10000 s	0 s	5100 s	27000 s	3000 s
SoftwareSystems-coreutils-NoOverflows 6 valid tasks (6 correct, 0 wrong, 71 void), max. score: 12		12	0	0	0	0	12	0	0
CPU time		280 s	0 s	0 s	0 s	0 s	230 s	0 s	0 s
SoftwareSystems-BusyBox-NoOverflows 70 valid tasks (6 correct, 64 wrong, 91 void), max. score: 105		70	0	0	0	0	70	0	0
CPU time		4300 s	0 s	0 s	0 s	0 s	8.3 s	0 s	0 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 7088 valid tasks (6913 correct, 175 wrong, 3460 void), max. score: 10632		2314	5832	0	1548	0	6975	6060	2467
CPU time		25000 s	120000 s	0 s	210000 s	0 s	97000 s	380000 s	79000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety 4 valid tasks (4 correct, 0 wrong, 2 void), max. score: 8		0	0	0	8	0	8	0	0
CPU time		0 s	0 s	0 s	180 s	0 s	380 s	0 s	0 s
SoftwareSystems-Intel-TDX-Module-ReachSafety 28 valid tasks (0 correct, 28 wrong, 3092 void), max. score: 28		0	0	0	0	0	0	0	0
CPU time		0 s	0 s	0 s	0 s	0 s	0 s	0 s	0 s
SoftwareSystems-Other-ReachSafety 14 valid tasks (9 correct, 5 wrong, 75 void), max. score: 21		6	9	0	3	0	8	5	5
CPU time		200 s	420 s	0 s	42 s	0 s	28 s	110 s	62 s
ValidationCrafted 3 valid tasks (3 correct, 0 wrong, 3 void), max. score: 6		6	0	0	0	0	0	6	0
CPU time		560 s	0 s	0 s	0 s	0 s	0 s	150 s	0 s
CorrectnessWitnesses-Loops 3 valid tasks (3 correct, 0 wrong, 3 void), max. score: 6		6	0	0	0	0	0	6	0
CPU time		560 s	0 s	0 s	0 s	0 s	0 s	150 s	0 s
Overall 53635 valid tasks (46690 correct, 6945 wrong, 27870 void), max. score: 87556		56546	15698	2637	-17005	-806	30743	57804	3488
CPU time		920000 s	130000 s	200000 s	860000 s	9300 s	340000 s	2100000 s	160000 s
Participants	Plots	CPAchecker	Goblint	LIV	MetaVal	MetaVal++	Mopsa	UAutomizer	UReferee

2. Validation of Violation Witnesses (Version 2.0)

Ranking by Category (with Score-Based Quantile Plots)

ReachSafety 1. Witch 2. CPAchecker 3. –	MemSafety 1. UAutomizer 2. Witch 3. CPAchecker	NoOverflows 1. UAutomizer 2. CPAchecker 3. Witch
SoftwareSystems 1. Witch 2. CPAchecker 3. MetaVal
ValidationCrafted 1. Witch 2. – 3. –	Overall 1. Witch 2. MetaVal 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	CPAchecker	MetaVal	UAutomizer	Witch
Representing Jury Member		Marian Lingsch-Rosenfeld	Marian Lingsch-Rosenfeld	Marcel Ebbinghaus	Paulína Ayaziová
Affiliation		LMU Munich, Germany	LMU Munich, Germany	University of Freiburg, Germany	Masaryk University, Brno, Czechia
ReachSafety 3548 valid tasks (3270 correct, 278 wrong, 7367 void), max. score: 4494		3081	-1406	-5438	3259
CPU time		54000 s	37000 s	51000 s	22000 s
ReachSafety-Arrays 145 valid tasks (116 correct, 29 wrong, 420 void), max. score: 218		218	72	112	192
CPU time		960 s	1400 s	2300 s	120 s
ReachSafety-BitVectors 38 valid tasks (36 correct, 2 wrong, 65 void), max. score: 57		49	-26	55	19
CPU time		170 s	270 s	810 s	110 s
ReachSafety-ControlFlow 56 valid tasks (56 correct, 0 wrong, 42 void), max. score: 56		26	26	-76	56
CPU time		230 s	360 s	900 s	48 s
ReachSafety-ECA 481 valid tasks (481 correct, 0 wrong, 984 void), max. score: 481		481	0	126	481
CPU time		11000 s	0 s	4700 s	3900 s
ReachSafety-Floats 55 valid tasks (55 correct, 0 wrong, 424 void), max. score: 55		55	51	29	8
CPU time		580 s	900 s	1500 s	15 s
ReachSafety-Heap 195 valid tasks (180 correct, 15 wrong, 340 void), max. score: 292		-78	74	124	266
CPU time		830 s	1200 s	4000 s	360 s
ReachSafety-Loops 355 valid tasks (223 correct, 132 wrong, 823 void), max. score: 532		54	119	-1529	519
CPU time		1600 s	2500 s	4200 s	1400 s
ReachSafety-ProductLines 479 valid tasks (479 correct, 0 wrong, 1189 void), max. score: 479		479	401	-12831	479
CPU time		5200 s	11000 s	90 s	4100 s
ReachSafety-Recursive 87 valid tasks (54 correct, 33 wrong, 284 void), max. score: 130		58	-1063	130	72
CPU time		700 s	360 s	1800 s	52 s
ReachSafety-Sequentialized 763 valid tasks (763 correct, 0 wrong, 576 void), max. score: 763		669	477	342	763
CPU time		10000 s	11000 s	20000 s	2500 s
ReachSafety-XCSP 98 valid tasks (98 correct, 0 wrong, 250 void), max. score: 98		98	72	14	98
CPU time		2300 s	2400 s	540 s	1300 s
ReachSafety-Combinations 497 valid tasks (477 correct, 20 wrong, 950 void), max. score: 746		746	514	571	693
CPU time		12000 s	4500 s	7400 s	4200 s
ReachSafety-Hardware 242 valid tasks (222 correct, 20 wrong, 654 void), max. score: 363		358	0	261	121
CPU time		7000 s	0 s	2500 s	3600 s
ReachSafety-Hardness 31 valid tasks (4 correct, 27 wrong, 320 void), max. score: 46		16	16	46	8
CPU time		42 s	93 s	730 s	12 s
ReachSafety-Fuzzle 26 valid tasks (26 correct, 0 wrong, 46 void), max. score: 26		26	16	0	26
CPU time		1400 s	970 s	0 s	570 s
MemSafety 107 valid tasks (91 correct, 16 wrong, 12886 void), max. score: 147		43	0	147	104
CPU time		160 s	0 s	1900 s	140 s
MemSafety-Arrays 44 valid tasks (36 correct, 8 wrong, 4040 void), max. score: 66		14	0	66	52
CPU time		100 s	0 s	780 s	51 s
MemSafety-Heap 31 valid tasks (27 correct, 4 wrong, 4222 void), max. score: 46		31	0	46	16
CPU time		25 s	0 s	520 s	25 s
MemSafety-LinkedLists 11 valid tasks (7 correct, 4 wrong, 2683 void), max. score: 16		3	0	16	13
CPU time		31 s	0 s	210 s	6.0 s
MemSafety-Other 21 valid tasks (21 correct, 0 wrong, 1941 void), max. score: 21		0	0	21	21
CPU time		0 s	0 s	390 s	62 s
NoOverflows 4706 valid tasks (4673 correct, 33 wrong, 15339 void), max. score: 5882		5010	0	5147	3900
CPU time		38000 s	0 s	98000 s	17000 s
NoOverflows-Main 628 valid tasks (595 correct, 33 wrong, 3454 void), max. score: 942		709	0	746	427
CPU time		3100 s	0 s	11000 s	2300 s
NoOverflows-Juliet 4078 valid tasks (4078 correct, 0 wrong, 11885 void), max. score: 4078		4078	0	4076	3985
CPU time		35000 s	0 s	87000 s	15000 s
SoftwareSystems 148 valid tasks (140 correct, 8 wrong, 2528 void), max. score: 222		74	73	-781	222
CPU time		2500 s	3500 s	720 s	420 s
SoftwareSystems-AWS-C-Common-ReachSafety 137 valid tasks (132 correct, 5 wrong, 280 void), max. score: 206		68	66	-504	206
CPU time		2300 s	3200 s	430 s	370 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 11 valid tasks (8 correct, 3 wrong, 2248 void), max. score: 16		6	6	-76	16
CPU time		170 s	260 s	300 s	49 s
ValidationCrafted 100 valid tasks (41 correct, 59 wrong, 0 void), max. score: 150		-700	0	-609	150
CPU time		300 s	0 s	1000 s	150 s
ViolationWitnesses-ControlFlow 100 valid tasks (41 correct, 59 wrong, 0 void), max. score: 150		-700	0	-609	150
CPU time		300 s	0 s	1000 s	150 s
Overall 8609 valid tasks (8215 correct, 394 wrong, 38120 void), max. score: 11866		-7179	162	-17958	9850
CPU time		95000 s	40000 s	150000 s	40000 s
Participants	Plots	CPAchecker	MetaVal	UAutomizer	Witch

3. Validation of Correctness Witnesses (Version 1.0)

Ranking by Category (with Score-Based Quantile Plots)

ReachSafety 1. UAutomizer 2. MetaVal 3. CPAchecker	NoOverflows 1. UAutomizer 2. CPAchecker 3. LIV	SoftwareSystems 1. UAutomizer 2. MetaVal 3. UReferee
Overall 1. UAutomizer 2. CPAchecker 3. MetaVal

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	LIV	MetaVal	UAutomizer	UReferee
Representing Jury Member		Marian Lingsch-Rosenfeld	Marian Lingsch-Rosenfeld	Marian Lingsch-Rosenfeld	Marcel Ebbinghaus	Frank Schüssele
Affiliation		LMU Munich, Germany	LMU Munich, Germany	LMU Munich, Germany	University of Freiburg, Germany	University of Freiburg, Germany
ReachSafety 39573 valid tasks (39543 correct, 30 wrong, 20456 void), max. score: 70152		40427	25398	49340	52303	7176
CPU time		1700000 s	380000 s	2700000 s	1400000 s	150000 s
ReachSafety-BitVectors 456 valid tasks (456 correct, 0 wrong, 99 void), max. score: 912		718	230	806	626	252
CPU time		15000 s	420 s	55000 s	30000 s	2300 s
ReachSafety-ControlFlow 238 valid tasks (237 correct, 1 wrong, 170 void), max. score: 357		228	63	198	341	127
CPU time		2600 s	400 s	3900 s	6000 s	13000 s
ReachSafety-ECA 3647 valid tasks (3647 correct, 0 wrong, 1056 void), max. score: 7294		6768	6760	46	6132	0
CPU time		230000 s	130000 s	3400 s	270000 s	0 s
ReachSafety-Loops 5934 valid tasks (5925 correct, 9 wrong, 3180 void), max. score: 8901		3645	834	8149	8401	1292
CPU time		120000 s	7600 s	410000 s	270000 s	25000 s
ReachSafety-ProductLines 3290 valid tasks (3290 correct, 0 wrong, 1056 void), max. score: 6580		1766	0	5868	6580	1220
CPU time		13000 s	0 s	560000 s	97000 s	26000 s
ReachSafety-Recursive 855 valid tasks (855 correct, 0 wrong, 357 void), max. score: 1710		136	430	1680	1626	0
CPU time		390 s	2000 s	9500 s	96000 s	0 s
ReachSafety-Sequentialized 176 valid tasks (173 correct, 3 wrong, 1376 void), max. score: 264		134	43	258	137	0
CPU time		12000 s	300 s	39000 s	4400 s	0 s
ReachSafety-XCSP 831 valid tasks (831 correct, 0 wrong, 58 void), max. score: 1662		1662	1662	1602	0	0
CPU time		17000 s	73000 s	28000 s	0 s	0 s
ReachSafety-Combinations 50 valid tasks (47 correct, 3 wrong, 897 void), max. score: 75		9	0	75	66	0
CPU time		3000 s	0 s	15000 s	6000 s	0 s
ReachSafety-Hardware 273 valid tasks (273 correct, 0 wrong, 1830 void), max. score: 546		440	186	0	546	78
CPU time		2100 s	580 s	0 s	21000 s	2500 s
ReachSafety-Hardness 23823 valid tasks (23809 correct, 14 wrong, 10377 void), max. score: 35734		23689	20686	25885	14938	864
CPU time		1200000 s	170000 s	1600000 s	590000 s	78000 s
NoOverflows 38846 valid tasks (38846 correct, 0 wrong, 18999 void), max. score: 77692		75470	16438	0	77578	0
CPU time		500000 s	20000 s	0 s	1000000 s	0 s
NoOverflows-Main 11627 valid tasks (11627 correct, 0 wrong, 6776 void), max. score: 23254		21924	9840	0	23186	0
CPU time		230000 s	20000 s	0 s	400000 s	0 s
NoOverflows-Juliet 27219 valid tasks (27219 correct, 0 wrong, 12223 void), max. score: 54438		54438	0	0	54438	0
CPU time		270000 s	0 s	0 s	610000 s	0 s
SoftwareSystems 13913 valid tasks (13893 correct, 20 wrong, 5666 void), max. score: 25507		10259	0	15487	20171	14072
CPU time		99000 s	0 s	1000000 s	830000 s	170000 s
SoftwareSystems-AWS-C-Common-ReachSafety 516 valid tasks (516 correct, 0 wrong, 1399 void), max. score: 1032		952	0	954	440	332
CPU time		42000 s	0 s	41000 s	31000 s	8300 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 13391 valid tasks (13371 correct, 20 wrong, 4209 void), max. score: 20086		4915	0	19961	20041	5235
CPU time		57000 s	0 s	990000 s	800000 s	160000 s
SoftwareSystems-Other-ReachSafety 6 valid tasks (6 correct, 0 wrong, 58 void), max. score: 12		0	0	0	12	12
CPU time		0 s	0 s	0 s	180 s	130 s
Overall 92332 valid tasks (92282 correct, 50 wrong, 45121 void), max. score: 172540		113930	32776	72634	146763	36711
CPU time		2200000 s	400000 s	3700000 s	3200000 s	320000 s
Participants	Plots	CPAchecker	LIV	MetaVal	UAutomizer	UReferee

4. Validation of Violation Witnesses (Version 1.0)

Ranking by Category (with Score-Based Quantile Plots)

ReachSafety 1. ConcurrentWitness2Test 2. – 3. –	MemSafety 1. CPAchecker 2. – 3. –	ConcurrencySafety 1. Dartagnan 2. CPAchecker 3. UAutomizer
NoOverflows 1. Symbiotic-Witch 2. – 3. –	Termination 1. CPAchecker 2. UAutomizer 3. –	SoftwareSystems 1. CPAchecker 2. Symbiotic-Witch 3. MetaVal

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	Hors Concours	Marian Lingsch-Rosenfeld	Hernán Ponce de León	Hors Concours	Marian Lingsch-Rosenfeld	Hors Concours	Paulína Ayaziová	Marcel Ebbinghaus
Affiliation		Budapest University of Technology and Economics, Hungary	--, --	LMU Munich, Germany	Huawei Dresden Research Center, Germany	--, --	LMU Munich, Germany	--, --	Masaryk University, Brno, Czechia	University of Freiburg, Germany
ReachSafety 20391 valid tasks (18141 correct, 2250 wrong, 25607 void), max. score: 29907		1931	6597	-17216		-10619	-22768	2021	-7630	-102982
CPU time		7900 s	140000 s	270000 s		36000 s	160000 s	11000 s	98000 s	320000 s
ReachSafety-Arrays 779 valid tasks (727 correct, 52 wrong, 1801 void), max. score: 1168		62	526	-435		277	-695	241	431	-6347
CPU time		260 s	4100 s	3900 s		830 s	8800 s	3400 s	970 s	6100 s
ReachSafety-BitVectors 242 valid tasks (219 correct, 23 wrong, 134 void), max. score: 363		45	106	-19		183	-224	26	-352	-587
CPU time		76 s	1200 s	1600 s		210 s	2600 s	2.5 s	900 s	4100 s
ReachSafety-ControlFlow 199 valid tasks (189 correct, 10 wrong, 271 void), max. score: 298		73	46	73		141	-909	15	-405	-46
CPU time		130 s	550 s	1200 s		180 s	1000 s	0.41 s	520 s	3200 s
ReachSafety-ECA 3862 valid tasks (3770 correct, 92 wrong, 2721 void), max. score: 5793		6	1457	2344		-4495	31	1799	1358	-28859
CPU time		33 s	65000 s	72000 s		16000 s	2600 s	6300 s	28000 s	62000 s
ReachSafety-Floats 644 valid tasks (415 correct, 229 wrong, 2405 void), max. score: 966		54	208	-1004		-1440	347	165	166	-1031
CPU time		75 s	1900 s	3200 s		510 s	6500 s	4.5 s	63 s	15000 s
ReachSafety-Heap 996 valid tasks (919 correct, 77 wrong, 516 void), max. score: 1494		-34	346	-1053		-1107	-549	262	-405	-3551
CPU time		500 s	3600 s	6700 s		910 s	10000 s	5.9 s	780 s	13000 s
ReachSafety-Loops 2213 valid tasks (1961 correct, 252 wrong, 3073 void), max. score: 3320		286	953	-2654		-1117	174	-399	1675	-13789
CPU time		2700 s	9100 s	12000 s		1900 s	20000 s	24 s	4600 s	24000 s
ReachSafety-ProductLines 3301 valid tasks (3261 correct, 40 wrong, 1947 void), max. score: 4952		311	0	-5611		3806	785	-1802	-14739	-22440
CPU time		1600 s	0 s	31000 s		4300 s	37000 s	64 s	28000 s	43000 s
ReachSafety-Recursive 452 valid tasks (385 correct, 67 wrong, 884 void), max. score: 678		168	203	105		106	-5806	-160	-876	-2839
CPU time		450 s	2200 s	3700 s		520 s	1100 s	110 s	380 s	4200 s
ReachSafety-Sequentialized 3097 valid tasks (2881 correct, 216 wrong, 1610 void), max. score: 4646		32	1170	407		560	773	1390	2180	-16003
CPU time		79 s	26000 s	45000 s		1400 s	40000 s	1000 s	11000 s	52000 s
ReachSafety-XCSP 687 valid tasks (634 correct, 53 wrong, 521 void), max. score: 1030		3	28	1029		275	-57	260	558	-3526
CPU time		4.7 s	820 s	16000 s		750 s	16000 s	22 s	13000 s	3400 s
ReachSafety-Combinations 2852 valid tasks (1865 correct, 987 wrong, 2343 void), max. score: 4278		0	615	-878		276	407	-619	706	-15447
CPU time		0 s	17000 s	42000 s		7200 s	13000 s	100 s	6200 s	70000 s
ReachSafety-Hardware 976 valid tasks (836 correct, 140 wrong, 3107 void), max. score: 1464		123	177	1344		-16	0	0	389	-4916
CPU time		2100 s	7000 s	26000 s		790 s	0 s	0 s	4500 s	12000 s
ReachSafety-Hardness 17 valid tasks (17 correct, 0 wrong, 4211 void), max. score: 17		0	13	-83		15	9	0	10	-215
CPU time		0 s	89 s	110 s		17 s	170 s	0 s	220 s	540 s
ReachSafety-Fuzzle 74 valid tasks (62 correct, 12 wrong, 63 void), max. score: 111		0	0	-409		-559	99	35	2	29
CPU time		0 s	0 s	2300 s		240 s	3000 s	57 s	12 s	1500 s
MemSafety 8810 valid tasks (6991 correct, 1819 wrong, 23228 void), max. score: 13215			-982	4455		-1141	0		-4867	-9764
CPU time			3800 s	68000 s		1200 s	0 s		13000 s	170000 s
MemSafety-Arrays 259 valid tasks (258 correct, 1 wrong, 328 void), max. score: 388			32	-245		-187	0		113	166
CPU time			540 s	1200 s		190 s	0 s		290 s	4400 s
MemSafety-Heap 784 valid tasks (662 correct, 122 wrong, 749 void), max. score: 1176			-358	-190		-644	0		-952	-3771
CPU time			2900 s	5400 s		760 s	0 s		710 s	7400 s
MemSafety-LinkedLists 153 valid tasks (122 correct, 31 wrong, 238 void), max. score: 230			-58	228		204	0		-800	-822
CPU time			340 s	1300 s		160 s	0 s		91 s	1500 s
MemSafety-Other 61 valid tasks (56 correct, 5 wrong, 156 void), max. score: 92			3	-11		38	0		90	59
CPU time			38 s	280 s		31 s	0 s		140 s	860 s
MemSafety-Juliet 7197 valid tasks (5582 correct, 1615 wrong, 21307 void), max. score: 10796			0	10774		0	0		7626	8143
CPU time			0 s	57000 s		0 s	0 s		12000 s	150000 s
MemSafety-MemCleanup 356 valid tasks (311 correct, 45 wrong, 450 void), max. score: 534			0	501		-424	0		58	283
CPU time			0 s	2800 s		45 s	0 s		310 s	8500 s
ConcurrencySafety 755 valid tasks (696 correct, 59 wrong, 12858 void), max. score: 1132				511	777					478
CPU time				5700 s	11000 s					18000 s
ConcurrencySafety-Main 531 valid tasks (515 correct, 16 wrong, 6104 void), max. score: 796		107		403	661					-1006
CPU time		220 s		4900 s	9100 s					12000 s
ConcurrencySafety-MemSafety 13 valid tasks (0 correct, 13 wrong, 2152 void), max. score: 26				4	22					26
CPU time				14 s	150 s					280 s
ConcurrencySafety-NoOverflows 52 valid tasks (52 correct, 0 wrong, 1714 void), max. score: 52				37	25					52
CPU time				290 s	200 s					1100 s
NoDataRace-Main 159 valid tasks (129 correct, 30 wrong, 2888 void), max. score: 238				148	111					227
CPU time				500 s	1100 s					4300 s
NoOverflows 17697 valid tasks (14206 correct, 3491 wrong, 30397 void), max. score: 26546			12104	-52463		-12560	0		3926	-14777
CPU time			97000 s	220000 s		19000 s	0 s		50000 s	320000 s
NoOverflows-Main 5324 valid tasks (5155 correct, 169 wrong, 3539 void), max. score: 7986			723	-12710		-10832	0		2102	-2188
CPU time			16000 s	33000 s		3900 s	0 s		23000 s	86000 s
NoOverflows-Juliet 12373 valid tasks (9051 correct, 3322 wrong, 26858 void), max. score: 18560			15243	-43821		7611	0		605	-15577
CPU time			81000 s	190000 s		15000 s	0 s		27000 s	230000 s
Termination 2057 valid tasks (2056 correct, 1 wrong, 4376 void), max. score: 2314				2314			0			2314
CPU time				34000 s			0 s			59000 s
Termination-BitVectors 45 valid tasks (45 correct, 0 wrong, 55 void), max. score: 45				45			0			45
CPU time				280 s			0 s			760 s
Termination-MainControlFlow 272 valid tasks (271 correct, 1 wrong, 458 void), max. score: 408				408			0			408
CPU time				2000 s			0 s			5500 s
Termination-MainHeap 8 valid tasks (8 correct, 0 wrong, 25 void), max. score: 8				8			0			8
CPU time				120 s			0 s			160 s
Termination-Other 1732 valid tasks (1732 correct, 0 wrong, 3838 void), max. score: 1732				1732			0			1732
CPU time				32000 s			0 s			53000 s
SoftwareSystems 1334 valid tasks (1019 correct, 315 wrong, 10024 void), max. score: 2001			225	1356		11	535	0	586	-606
CPU time			2400 s	21000 s		900 s	20000 s	0 s	1400 s	19000 s
SoftwareSystems-AWS-C-Common-ReachSafety 638 valid tasks (526 correct, 112 wrong, 1451 void), max. score: 957			0	501		15	-43	0	521	-5643
CPU time			0 s	8700 s		880 s	13000 s	0 s	1200 s	5000 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 303 valid tasks (157 correct, 146 wrong, 5408 void), max. score: 454			0	251		0	417	0	0	333
CPU time			0 s	6300 s		0 s	7700 s	0 s	0 s	9300 s
SoftwareSystems-DeviceDriversLinux64-MemSafety 149 valid tasks (140 correct, 9 wrong, 945 void), max. score: 224			64	224		5	0	0	2	159
CPU time			2000 s	1800 s		15 s	0 s	0 s	5.5 s	1400 s
SoftwareSystems-Other-ReachSafety 3 valid tasks (1 correct, 2 wrong, 143 void), max. score: 4			0	2		0	4	0	0	3
CPU time			0 s	77 s		0 s	67 s	0 s	0 s	110 s
SoftwareSystems-uthash-MemSafety 84 valid tasks (60 correct, 24 wrong, 953 void), max. score: 126			63	42		0	0	0	63	84
CPU time			370 s	1000 s		0 s	0 s	0 s	89 s	990 s
SoftwareSystems-uthash-MemCleanup 66 valid tasks (48 correct, 18 wrong, 588 void), max. score: 99			0	99		0	0	0	99	0
CPU time			0 s	1600 s		0 s	0 s	0 s	75 s	0 s
SoftwareSystems-DeviceDriversLinux64-Termination 91 valid tasks (87 correct, 4 wrong, 536 void), max. score: 136			0	136		0	0	0	0	136
CPU time			0 s	1300 s		0 s	0 s	0 s	0 s	2000 s
Overall 51044 valid tasks (43109 correct, 7935 wrong, 106490 void), max. score: 73092				-4127						-48406
CPU time				620000 s						900000 s
Participants	Plots	ConcurrentWitness2Test	CPA-witness2test	CPAchecker	Dartagnan	CProver-witness2test	MetaVal	NITWIT	Symbiotic-Witch	UAutomizer

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 webmaster).