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

Results of the Competition on Witness Validation

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

• Proposal of Validation Track and Scoring Schema (Proc. SAS 2022)
• 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 2022 results archive, which contains all data that I obtained with BenchExec and from which I compiled all the tables and aggregated data displays. For the most detailed tables, which end on ".xml.bz2.table.html", you can obtain the raw data by accessing the URL with the ".table.html" removed.
• Falsification: Here only bug hunting matters and proof generation is ignored. There are no different results tables for the Falsification category because all verification tasks (except Termination) are included, but the TRUE results are ignored (no score assigned). If you want to remove for a particular verifier the TRUE results, proceed as follows: Click in the menu on "Filter Rows". Then select "status" for the verifier you are interested in for row selection, then a choose box with all the status-values appears. There you choose "true" and then click "invert filter".
• More on table generation is described here.
• Column "score" shows the (not normalized) score assigned to the result of the verification task.
• Column "witness" contains a link to the witness file for download/display.
• Column "inspect witness" opens a new page that displays information about the witness an a list of witnesses that other verifiers produced for the same program.
• Column "cpu" shows the consumed CPU time.
• Column "wall" shows the elapsed wall time.
• Column "energy" shows the energy consumed by the CPU.
• Column "mem" shows the peak memory usage.
• Column "blkio-w" shows the accumulated amount of information written to block devices.
• Column "blkio-r" shows the accumulated amount of information read from block devices.
• More information on results.

Contents

1. Validation of Violation Witnesses
2. Validation of Correctness Witnesses

1. Validation of Violation Witnesses

Ranking by Category (with Score-Based Quantile Plots)

ReachSafety 1. UAutomizer 2. CProver-witness2test 3. CPAchecker	MemSafety 1. UAutomizer 2. CPAchecker 3. CPA-witness2test	ConcurrencySafety 1. Dartagnan 2. CPAchecker 3. UAutomizer
NoOverflows 1. UAutomizer 2. CProver-witness2test 3. CPAchecker	Termination 1. UAutomizer 2. CPAchecker 3. MetaVal	SoftwareSystems 1. Symbiotic-Witch 2. UAutomizer 3. CPAchecker
Overall 1. UAutomizer 2. CPAchecker 3. Symbiotic-Witch

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. SAS 2022] and the categories are defined on the respective SV-COMP web page.

Hide base categories

Participants	Plots	CPAchecker	CPA-witness2test	Dartagnan	CProver-witness2test	GWIT	MetaVal	NITWIT	Symbiotic-Witch	UAutomizer	WIT4JAVA
Representing Jury Member		Henrik Wachowitz	Henrik Wachowitz	Hernán Ponce de León	Michael Tautschnig	Falk Howar	Martin Spiessl	Jana (Philipp) Berger	Paulína Ayaziová	Daniel Dietsch	Tong Wu
Affiliation		LMU Munich, Germany	LMU Munich, Germany	Huawei Dresden Research Center, Germany	Queen Mary University of London, UK	TU Dortmund University, Germany	LMU Munich, Germany	RWTH Aachen, Germany	Masaryk University, Brno, Czechia	University of Freiburg, Germany	University of Manchester, UK
ReachSafety 36231 valid tasks (30763 correct, 5468 wrong, 512 void), max. score: 90578		33938	12336		49545		24807	8869	28290	62966
CPU time		330000 s	150000 s		59000 s		190000 s	9100 s	150000 s	360000 s
ReachSafety-Arrays 2035 valid tasks (1505 correct, 530 wrong, 0 void), max. score: 5088		590	672		2948		478	871	970	4389
CPU time		6400 s	2900 s		1400 s		13000 s	500 s	2200 s	19000 s
ReachSafety-BitVectors 357 valid tasks (286 correct, 71 wrong, 12 void), max. score: 892		545	220		658		251	134	386	760
CPU time		2000 s	960 s		340 s		2500 s	2.7 s	1400 s	5800 s
ReachSafety-ControlFlow 127 valid tasks (108 correct, 19 wrong, 2 void), max. score: 318		187	22		222		51	13	78	270
CPU time		670 s	310 s		100 s		380 s	0.30 s	680 s	1200 s
ReachSafety-ECA 6613 valid tasks (5444 correct, 1169 wrong, 1 void), max. score: 16533		5677	1653		12864		21	2587	1850	11189
CPU time		90000 s	68000 s		30000 s		1600 s	6900 s	38000 s	90000 s
ReachSafety-Floats 1257 valid tasks (729 correct, 528 wrong, 18 void), max. score: 3143		961	877		2024		1633	-305	1433	720
CPU time		5000 s	2900 s		1100 s		11000 s	6.0 s	220 s	12000 s
ReachSafety-Heap 1208 valid tasks (1073 correct, 135 wrong, 19 void), max. score: 3020		285	891		2135		1218	209	1319	1976
CPU time		5600 s	2600 s		1200 s		13000 s	4.7 s	1100 s	9000 s
ReachSafety-Loops 4494 valid tasks (3511 correct, 983 wrong, 46 void), max. score: 11235		3937	1730		6872		4390	1511	6089	9602
CPU time		18000 s	7800 s		3500 s		47000 s	29 s	9700 s	39000 s
ReachSafety-ProductLines 5414 valid tasks (4697 correct, 717 wrong, 222 void), max. score: 13535		12287	0		5200		787	2129	3196	11485
CPU time		48000 s	0 s		7500 s		33000 s	80 s	44000 s	44000 s
ReachSafety-Recursive 538 valid tasks (473 correct, 65 wrong, 0 void), max. score: 1345		82	431		1163		1080	204	522	1147
CPU time		2900 s	1100 s		690 s		640 s	140 s	930 s	3300 s
ReachSafety-Sequentialized 4686 valid tasks (4463 correct, 223 wrong, 54 void), max. score: 11715		2744	1062		874		882	1555	2461	9349
CPU time		45000 s	23000 s		1800 s		37000 s	1200 s	14000 s	56000 s
ReachSafety-XCSP 917 valid tasks (857 correct, 60 wrong, 43 void), max. score: 2293		1802	25		342		1725	304	1568	1629
CPU time		18000 s	800 s		1300 s		18000 s	87 s	11000 s	7500 s
ReachSafety-Combinations 5253 valid tasks (4822 correct, 431 wrong, 71 void), max. score: 13132		3094	597		11556		269	970	911	8933
CPU time		62000 s	29000 s		10000 s		15000 s	100 s	19000 s	53000 s
ReachSafety-Hardware 3332 valid tasks (2795 correct, 537 wrong, 24 void), max. score: 8330		1968	235		0		0	0	473	1397
CPU time		29000 s	13000 s		0 s		0 s	0 s	7200 s	18000 s
MemSafety 18856 valid tasks (17215 correct, 1641 wrong, 60 void), max. score: 47140		9013	1241		-11363		0		-2134	31156
CPU time		140000 s	2700 s		1600 s		0 s		17000 s	180000 s
MemSafety-Arrays 233 valid tasks (208 correct, 25 wrong, 1 void), max. score: 583		-241	23		-675		0		-505	535
CPU time		570 s	290 s		170 s		0 s		210 s	4300 s
MemSafety-Heap 1005 valid tasks (938 correct, 67 wrong, 38 void), max. score: 2512		1	94		-1366		0		-886	1948
CPU time		5500 s	1700 s		850 s		0 s		580 s	6600 s
MemSafety-LinkedLists 303 valid tasks (271 correct, 32 wrong, 13 void), max. score: 757		206	15		97		0		113	360
CPU time		1800 s	230 s		340 s		0 s		150 s	490 s
MemSafety-Other 285 valid tasks (272 correct, 13 wrong, 3 void), max. score: 713		113	44		85		0		94	620
CPU time		1400 s	530 s		210 s		0 s		140 s	2600 s
MemSafety-Juliet 16500 valid tasks (14998 correct, 1502 wrong, 0 void), max. score: 41250		40542	0		0		0		6138	34415
CPU time		130000 s	0 s		0 s		0 s		16000 s	150000 s
MemSafety-MemCleanup 530 valid tasks (528 correct, 2 wrong, 5 void), max. score: 1325		196			13		0		685	122
CPU time		2500 s			37 s		0 s		210 s	7200 s
ConcurrencySafety 13400 valid tasks (5525 correct, 7875 wrong, 152 void), max. score: 31825		2658		9777						912
CPU time		52000 s		160000 s						4500 s
ConcurrencySafety-Main 6515 valid tasks (5205 correct, 1310 wrong, 39 void), max. score: 16287		3327		7465						0
CPU time		52000 s		130000 s						0 s
ConcurrencySafety-MemSafety 2920 valid tasks (0 correct, 2920 wrong, 34 void), max. score: 5840				0						0
CPU time				0 s						0 s
ConcurrencySafety-NoOverflows 2032 valid tasks (99 correct, 1933 wrong, 36 void), max. score: 5080		575		0						553
CPU time		430 s		0 s						4500 s
NoDataRace-Main 1933 valid tasks (221 correct, 1712 wrong, 43 void), max. score: 4832		0		3426						0
CPU time		0 s		26000 s						0 s
NoOverflows 31813 valid tasks (27691 correct, 4122 wrong, 3087 void), max. score: 79532		28600	3638		61848		0		25971	74933
CPU time		18000 s	5200 s		23000 s		0 s		65000 s	530000 s
NoOverflows-Main 3628 valid tasks (3285 correct, 343 wrong, 322 void), max. score: 9070		6523	830		6989		0		2962	8805
CPU time		18000 s	5200 s		2900 s		0 s		11000 s	54000 s
NoOverflows-Juliet 28185 valid tasks (24406 correct, 3779 wrong, 2765 void), max. score: 70462		0	0		55294		0		23009	64370
CPU time		0 s	0 s		20000 s		0 s		54000 s	480000 s
Termination 4953 valid tasks (4922 correct, 31 wrong, 410 void), max. score: 9906		423					0			3017
CPU time		67000 s					0 s			27000 s
Termination-BitVectors 52 valid tasks (44 correct, 8 wrong, 7 void), max. score: 130										86
CPU time										370 s
Termination-MainControlFlow 328 valid tasks (313 correct, 15 wrong, 47 void), max. score: 820							0			106
CPU time							0 s			4300 s
Termination-MainHeap 4 valid tasks (4 correct, 0 wrong, 1 void), max. score: 2		0					0			2
CPU time		0 s					0 s			75 s
Termination-Other 4569 valid tasks (4561 correct, 8 wrong, 355 void), max. score: 11423		1559					0			415
CPU time		67000 s					0 s			23000 s
SoftwareSystems 7933 valid tasks (2376 correct, 5557 wrong, 31 void), max. score: 15866		1620	1216		-7322		925		3304	2468
CPU time		49000 s	2100 s		1100 s		21000 s		2000 s	110000 s
SoftwareSystems-AWS-C-Common-ReachSafety 438 valid tasks (53 correct, 385 wrong, 5 void), max. score: 1095		267	0		207		174	0	511	703
CPU time		3100 s	0 s		220 s		2400 s	0 s	1200 s	7700 s
SoftwareSystems-BusyBox-ReachSafety 9 valid tasks (9 correct, 0 wrong, 0 void), max. score: 5		0	0		0		0	0	0	0
CPU time		33 s	0 s		0 s		19 s	0 s	0 s	0 s
SoftwareSystems-BusyBox-MemSafety 83 valid tasks (28 correct, 55 wrong, 1 void), max. score: 207		16	0		-485		0		-2	18
CPU time		73 s	0 s		31 s		0 s		45 s	220 s
SoftwareSystems-BusyBox-NoOverflows 75 valid tasks (44 correct, 31 wrong, 0 void), max. score: 187		10	0		6		0		5	10
CPU time		64 s	0 s		4.3 s		0 s		2.7 s	41 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 5548 valid tasks (1091 correct, 4457 wrong, 22 void), max. score: 13870		4854	15		1095		1490	0	12	8089
CPU time		39000 s	48 s		770 s		15000 s	0 s	9.5 s	97000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety 14 valid tasks (0 correct, 14 wrong, 0 void), max. score: 28		0	0		0		0	0	0	0
CPU time		0 s	0 s		0 s		0 s	0 s	0 s	0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety 532 valid tasks (532 correct, 0 wrong, 0 void), max. score: 266		138	19		7		0		4	6
CPU time		3700 s	560 s		33 s		0 s		25 s	490 s
SoftwareSystems-OpenBSD-MemSafety 22 valid tasks (19 correct, 3 wrong, 3 void), max. score: 55		0	0		-112		0		0	0
CPU time		0 s	0 s		35 s		0 s		0 s	0 s
SoftwareSystems-uthash-ReachSafety 342 valid tasks (0 correct, 342 wrong, 0 void), max. score: 684		0	0		0		192	0	408	0
CPU time		0 s	0 s		0 s		3300 s	0 s	190 s	0 s
SoftwareSystems-uthash-MemSafety 666 valid tasks (600 correct, 66 wrong, 0 void), max. score: 1665		80	0		0		0		113	0
CPU time		2900 s	0 s		0 s		0 s		320 s	0 s
SoftwareSystems-uthash-NoOverflows 204 valid tasks (0 correct, 204 wrong, 0 void), max. score: 408		0	336		0		0		408	0
CPU time		0 s	1500 s		0 s		0 s		220 s	0 s
Overall 113186 valid tasks (88492 correct, 24694 wrong, 4252 void), max. score: 261743		52851	12712	13764	33690		15116	4618	35851	127030
CPU time		660000 s	160000 s	160000 s	84000 s		210000 s	9100 s	230000 s	1200000 s
Participants	Plots	CPAchecker	CPA-witness2test	Dartagnan	CProver-witness2test	GWIT	MetaVal	NITWIT	Symbiotic-Witch	UAutomizer	WIT4JAVA

2. Validation of Correctness Witnesses

Ranking by Category (with Score-Based Quantile Plots)

ReachSafety 1. CPAchecker 2. UAutomizer 3. MetaVal	MemSafety 1. UAutomizer 2. MetaVal 3. –	ConcurrencySafety 1. UAutomizer 2. – 3. –
NoOverflows 1. UAutomizer 2. CPAchecker 3. MetaVal	Termination 1. – 2. – 3. –	SoftwareSystems 1. UAutomizer 2. CPAchecker 3. MetaVal
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. SAS 2022] and the categories are defined on the respective SV-COMP web page.

Hide base categories

Participants	Plots	CPAchecker	MetaVal	UAutomizer
Representing Jury Member		Henrik Wachowitz	Martin Spiessl	Daniel Dietsch
Affiliation		LMU Munich, Germany	LMU Munich, Germany	University of Freiburg, Germany
ReachSafety 36231 valid tasks (30763 correct, 5468 wrong, 512 void), max. score: 90578		34487	-135674	33342
CPU time		810000 s	1100000 s	1300000 s
ReachSafety-Arrays 2035 valid tasks (1505 correct, 530 wrong, 0 void), max. score: 5088		17	-1687	758
CPU time		95 s	3300 s	3800 s
ReachSafety-BitVectors 357 valid tasks (286 correct, 71 wrong, 12 void), max. score: 892		542	596	493
CPU time		16000 s	53000 s	14000 s
ReachSafety-ControlFlow 127 valid tasks (108 correct, 19 wrong, 2 void), max. score: 318		162	-5137	168
CPU time		1200 s	1900 s	4000 s
ReachSafety-ECA 6613 valid tasks (5444 correct, 1169 wrong, 1 void), max. score: 16533		3369	17	4209
CPU time		320000 s	3700 s	310000 s
ReachSafety-Floats 1257 valid tasks (729 correct, 528 wrong, 18 void), max. score: 3143		7918	-5541	5269
CPU time		89000 s	190000 s	370000 s
ReachSafety-Heap 1208 valid tasks (1073 correct, 135 wrong, 19 void), max. score: 3020		700	-1795	1123
CPU time		18000 s	35000 s	19000 s
ReachSafety-Loops 4494 valid tasks (3511 correct, 983 wrong, 46 void), max. score: 11235		2763	1263	7256
CPU time		120000 s	280000 s	270000 s
ReachSafety-ProductLines 5414 valid tasks (4697 correct, 717 wrong, 222 void), max. score: 13535		1746	2641	2949
CPU time		100000 s	510000 s	94000 s
ReachSafety-Recursive 538 valid tasks (473 correct, 65 wrong, 0 void), max. score: 1345		0	-2606	229
CPU time		0 s	2600 s	17000 s
ReachSafety-Sequentialized 4686 valid tasks (4463 correct, 223 wrong, 54 void), max. score: 11715		740	232	97
CPU time		110000 s	33000 s	10000 s
ReachSafety-XCSP 917 valid tasks (857 correct, 60 wrong, 43 void), max. score: 2293		896	752	0
CPU time		18000 s	25000 s	0 s
ReachSafety-Combinations 5253 valid tasks (4822 correct, 431 wrong, 71 void), max. score: 13132		10	112	268
CPU time		4100 s	10000 s	39000 s
ReachSafety-Hardware 3332 valid tasks (2795 correct, 537 wrong, 24 void), max. score: 8330		366	0	1584
CPU time		7500 s	0 s	110000 s
MemSafety 18856 valid tasks (17215 correct, 1641 wrong, 60 void), max. score: 47140			0	13975
CPU time			0 s	2600000 s
MemSafety-Arrays 233 valid tasks (208 correct, 25 wrong, 1 void), max. score: 583			0	311
CPU time			0 s	5000 s
MemSafety-Heap 1005 valid tasks (938 correct, 67 wrong, 38 void), max. score: 2512			0	533
CPU time			0 s	33000 s
MemSafety-LinkedLists 303 valid tasks (271 correct, 32 wrong, 13 void), max. score: 757			0	82
CPU time			0 s	930 s
MemSafety-Other 285 valid tasks (272 correct, 13 wrong, 3 void), max. score: 713			0	227
CPU time			0 s	5000 s
MemSafety-Juliet 16500 valid tasks (14998 correct, 1502 wrong, 0 void), max. score: 41250			0	24197
CPU time			0 s	2500000 s
MemSafety-MemCleanup 530 valid tasks (528 correct, 2 wrong, 5 void), max. score: 1325			0	27
CPU time			0 s	860 s
ConcurrencySafety 13400 valid tasks (5525 correct, 7875 wrong, 152 void), max. score: 31825				26691
CPU time				490000 s
ConcurrencySafety-Main 6515 valid tasks (5205 correct, 1310 wrong, 39 void), max. score: 16287				3028
CPU time				130000 s
ConcurrencySafety-MemSafety 2920 valid tasks (0 correct, 2920 wrong, 34 void), max. score: 5840				1979
CPU time				82000 s
ConcurrencySafety-NoOverflows 2032 valid tasks (99 correct, 1933 wrong, 36 void), max. score: 5080				13868
CPU time				280000 s
NoDataRace-Main 1933 valid tasks (221 correct, 1712 wrong, 43 void), max. score: 4832
CPU time
NoOverflows 31813 valid tasks (27691 correct, 4122 wrong, 3087 void), max. score: 79532		23297	0	61391
CPU time		52000 s	0 s	1400000 s
NoOverflows-Main 3628 valid tasks (3285 correct, 343 wrong, 322 void), max. score: 9070		5314	0	6453
CPU time		52000 s	0 s	110000 s
NoOverflows-Juliet 28185 valid tasks (24406 correct, 3779 wrong, 2765 void), max. score: 70462		0	0	58649
CPU time		0 s	0 s	1300000 s
Termination 4953 valid tasks (4922 correct, 31 wrong, 410 void), max. score: 9906
CPU time
Termination-BitVectors 52 valid tasks (44 correct, 8 wrong, 7 void), max. score: 130
CPU time
Termination-MainControlFlow 328 valid tasks (313 correct, 15 wrong, 47 void), max. score: 820
CPU time
Termination-MainHeap 4 valid tasks (4 correct, 0 wrong, 1 void), max. score: 2
CPU time
Termination-Other 4569 valid tasks (4561 correct, 8 wrong, 355 void), max. score: 11423
CPU time
SoftwareSystems 7933 valid tasks (2376 correct, 5557 wrong, 31 void), max. score: 15866		3408	-107006	3418
CPU time		130000 s	2100000 s	1100000 s
SoftwareSystems-AWS-C-Common-ReachSafety 438 valid tasks (53 correct, 385 wrong, 5 void), max. score: 1095		766	-22339	466
CPU time		31000 s	65000 s	60000 s
SoftwareSystems-BusyBox-ReachSafety 9 valid tasks (9 correct, 0 wrong, 0 void), max. score: 5		0	-350	0
CPU time		0 s	38 s	0 s
SoftwareSystems-BusyBox-MemSafety 83 valid tasks (28 correct, 55 wrong, 1 void), max. score: 207			0	0
CPU time			0 s	0 s
SoftwareSystems-BusyBox-NoOverflows 75 valid tasks (44 correct, 31 wrong, 0 void), max. score: 187		147	0	35
CPU time		9900 s	0 s	790 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 5548 valid tasks (1091 correct, 4457 wrong, 22 void), max. score: 13870		5656	-337506	17805
CPU time		89000 s	2000000 s	1000000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety 14 valid tasks (0 correct, 14 wrong, 0 void), max. score: 28		0	13	0
CPU time		0 s	1300 s	0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety 532 valid tasks (532 correct, 0 wrong, 0 void), max. score: 266			0	1
CPU time			0 s	55 s
SoftwareSystems-OpenBSD-MemSafety 22 valid tasks (19 correct, 3 wrong, 3 void), max. score: 55			0	0
CPU time			0 s	0 s
SoftwareSystems-uthash-ReachSafety 342 valid tasks (0 correct, 342 wrong, 0 void), max. score: 684		0	486	0
CPU time		0 s	30000 s	0 s
SoftwareSystems-uthash-MemSafety 666 valid tasks (600 correct, 66 wrong, 0 void), max. score: 1665			0	0
CPU time			0 s	0 s
SoftwareSystems-uthash-NoOverflows 204 valid tasks (0 correct, 204 wrong, 0 void), max. score: 408		0	0	0
CPU time		0 s	0 s	0 s
Overall 113186 valid tasks (88492 correct, 24694 wrong, 4252 void), max. score: 261743		39875	-325096	113448
CPU time		990000 s	3300000 s	6800000 s
Participants	Plots	CPAchecker	MetaVal	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 chair).