FASE 2023
5th Competition on Software Testing (Test-Comp 2023)

Results of the Competition

This web page presents the results of Test-Comp 2023 - 5th International Competition on Software Testing.

• Competition Report for Test-Comp 2023
• 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 reading the score-based quantile plots:

• A data point (x, y) tells you that the quantile of cumulative score x can be achieved with a minimum of y tasks.
• The right end of the graph displays the achieved score. The score is the competition's definition of quality. You can read the ranking on the top from right to left.
• More information on what to learn from and how to interpret score-based quantile plots can be found in the SV-COMP '15 report on pages 12 and 13.

Here some brief directions for navigating in the BenchExec-generated tables with the results:

• Please note the header with the menu "Select Columns, Filter Rows, etc.", which loads only after all data are retrieved from the server.
• The tables contain all information that I thought you could be interested in. If there are too many columns, you can get rid of some with "Select Columns". You can also investigate special classes of rows using "Filter Rows".
• If you want to see more data, including the time and memory needed for validation, please click on the score value in the table below (works only for base categories) to browse the most detailed tables, which also contain links to obtain the test-suites that the test-generator generated.
• In all results tables, the sources of the verification task is available via click on "prog". The log files are available via click on the status (result).
• If you want to investigate even more, you can download the Test-Comp 2023 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 task.
• Column "test-suite" contains a link to the test-suite archive for download/display.
• Column "inspect test-suite" opens a new page that displays information about the test-suite an a list of test-suites that other test-generators 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 the results are available in the FAQ.

Ranking by Category (with Score-Based Quantile Plots)

Cover-Error 1. FuSeBMC 2. VeriFuzz 3. FuSeBMC_IA	Cover-Branches 1. FuSeBMC 2. VeriFuzz 3. FuSeBMC_IA	Overall 1. FuSeBMC 2. VeriFuzz 3. FuSeBMC_IA

Table of All Results

In every table cell for competition results, we list the points in the first row and the CPU time (rounded to two significant digits) for successful runs in the second row.

The entry 'Hors Concours' in the row for 'Representing Jury Member' means that the tool was added at the organizer's disposition and does not participate in the rankings or prize allocation.
The entry '–' means that the competition candidate opted-out in the category.
The definition of the scoring schema and the categories is given on the respective SV-COMP web pages.

Hide base categories

Participants	Plots	CoVeriTest	ESBMC-kind	FuSeBMC	FuSeBMC_IA	HybridTiger	KLEE	Legion	Legion/SymCC	PRTest	Symbiotic	TracerX	VeriFuzz	WASP-C
Representing Jury Member		Marie-Christine Jakobs	Rafael Sá Menezes	Kaled Alshmrany	Mohannad Aldughaim	Hors Concours	Hors Concours	Hors Concours	Gidon Ernst	Thomas Lemberger	Marek Trtík	Joxan Jaffar	Raveendra Kumar Medicherla	Filipe Marques
Affiliation		TU Darmstadt, Germany	University of Manchester, UK	University of Manchester / Institute of Public Administration, UK / Saudi Arabia	University of Manchester / King Saud University, UK / Saudi Arabia	--, --	--, --	--, --	LMU Munich, Germany	QAware GmbH, Germany	Masaryk University, Brno, Czechia	National University of Singapore, Singapore	Tata Consultancy Services, India	INESC-ID, Lisbon, Portugal
Cover-Error 1173 tasks		581	289	936	908	463	721		349	222	644		909	570
CPU time		120000 s	3100 s	260000 s	130000 s	240000 s	10000 s		2700 s	240000 s	20000 s		16000 s	9300 s
ReachSafety-Arrays 90 tasks		71	5	90	88	67	85	67	19	36	72	0	88	78
CPU time		12000 s	44 s	15000 s	13000 s	40000 s	110 s	60000 s	17 s	5000 s	630 s	0 s	510 s	410 s
ReachSafety-BitVectors 9 tasks		7	0	9	9	5	8	1	3	5	7	0	9	7
CPU time		250 s	0 s	880 s	880 s	1400 s	5.5 s	300 s	890 s	4500 s	88 s	0 s	340 s	500 s
ReachSafety-ControlFlow 5 tasks		1	0	5	5	0	4	0	3	0	5	0	4	4
CPU time		910 s	0 s	450 s	460 s	0 s	1.9 s	0 s	480 s	0 s	140 s	0 s	330 s	97 s
ReachSafety-ECA 18 tasks		3	0	12	11	1	14	0	1	0	13	0	14	2
CPU time		390 s	0 s	2100 s	2000 s	900 s	490 s	0 s	1.3 s	0 s	900 s	0 s	840 s	180 s
ReachSafety-Floats 32 tasks		24	13	32	31	22	7	0	2	2	0	0	31	22
CPU time		2800 s	96 s	4500 s	3100 s	4600 s	2.8 s	0 s	8.1 s	1800 s	0 s	0 s	420 s	2800 s
ReachSafety-Heap 47 tasks		42	6	45	45	37	45	3	42	11	45	0	45	36
CPU time		13000 s	1.0 s	1800 s	1800 s	9100 s	170 s	18 s	690 s	9900 s	190 s	0 s	260 s	760 s
ReachSafety-Loops 130 tasks		64	70	128	127	47	82	3	34	89	71	0	123	96
CPU time		36000 s	910 s	28000 s	28000 s	30000 s	3400 s	2700 s	70 s	80000 s	2700 s	0 s	2400 s	770 s
ReachSafety-ProductLines 169 tasks		160	169	169	169	45	169	34	159	92	159	0	169	5
CPU time		39000 s	380 s	1000 s	1000 s	41000 s	82 s	210 s	360 s	83000 s	3100 s	0 s	1300 s	37 s
ReachSafety-Recursive 20 tasks		7	0	19	19	5	16	0	16	1	17	0	18	12
CPU time		3100 s	0 s	870 s	1300 s	680 s	8.8 s	0 s	150 s	900 s	230 s	0 s	330 s	41 s
ReachSafety-Sequentialized 98 tasks		55	40	94	92	86	78	0	0	0	71	0	95	43
CPU time		4300 s	60 s	11000 s	9900 s	75000 s	3600 s	0 s	0 s	0 s	4000 s	0 s	1000 s	810 s
ReachSafety-XCSP 54 tasks		45	49	47	47	47	32	0	0	0	16	0	49	49
CPU time		2200 s	1600 s	1200 s	1200 s	22000 s	2500 s	0 s	0 s	0 s	6700 s	0 s	1100 s	1800 s
ReachSafety-Hardware 494 tasks		85	0	288	288	35	0	0	1	57	34	0	319	39
CPU time		11000 s	0 s	190000 s	69000 s	20000 s	0 s	0 s	1.2 s	51000 s	930 s	0 s	7400 s	1100 s
SoftwareSystems-BusyBox-MemSafety 5 tasks		0	0	1	0	0	1	0	0	0	0	0	0	0
CPU time		0 s	0 s	280 s	0 s	0 s	1.8 s	0 s	0 s	0 s	0 s	0 s	0 s	0 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 2 tasks		0	0	0	0	0	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	0 s	0 s	0 s	0 s	0 s
Cover-Branches 2933 tasks		1509		1678	1538	1170	999	838	1027	770	1430	1400	1546	1103
CPU time		1700000 s		2600000 s	1700000 s	1600000 s	990000 s	2300000 s	2500000 s	2400000 s	1600000 s	780000 s	2600000 s	1100000 s
ReachSafety-Arrays 292 tasks		208		253	249	202	73	171	99	127	204	200	238	191
CPU time		240000 s		260000 s	170000 s	240000 s	34000 s	210000 s	250000 s	110000 s	230000 s	81000 s	250000 s	140000 s
ReachSafety-BitVectors 61 tasks		48		48	42	16	31	33	44	33	48	48	45	34
CPU time		20000 s		55000 s	28000 s	7400 s	22000 s	51000 s	40000 s	54000 s	36000 s	33000 s	55000 s	29000 s
ReachSafety-ControlFlow 11 tasks		0		2	1	0	1	0	1	0	1	1	1	1
CPU time		7000 s		9200 s	3800 s	5800 s	800 s	8100 s	9900 s	2900 s	1400 s	14 s	9000 s	1200 s
ReachSafety-ECA 29 tasks		5		9	9	2	7	3	3	2	9	7	10	4
CPU time		24000 s		26000 s	24000 s	23000 s	26000 s	21000 s	19000 s	26000 s	21000 s	14000 s	25000 s	24000 s
ReachSafety-Floats 197 tasks		92		100	96	76	16	54	48	40	47	45	98	53
CPU time		63000 s		180000 s	71000 s	62000 s	11000 s	160000 s	170000 s	180000 s	6300 s	490 s	180000 s	26000 s
ReachSafety-Heap 110 tasks		76		80	79	63	74	61	77	34	74	77	78	63
CPU time		75000 s		98000 s	54000 s	47000 s	65000 s	80000 s	95000 s	57000 s	69000 s	12000 s	99000 s	39000 s
ReachSafety-Loops 661 tasks		526		543	534	431	356	319	242	325	502	504	538	381
CPU time		420000 s		600000 s	300000 s	360000 s	190000 s	500000 s	570000 s	590000 s	260000 s	160000 s	590000 s	170000 s
ReachSafety-ProductLines 263 tasks		76		77	77	55	74	70	73	48	69	77	77	1
CPU time		61000 s		200000 s	170000 s	220000 s	9800 s	190000 s	160000 s	240000 s	5500 s	10000 s	240000 s	1800 s
ReachSafety-Recursive 51 tasks		40		44	43	37	21	26	39	10	44	39	39	37
CPU time		46000 s		46000 s	25000 s	27000 s	21000 s	20000 s	46000 s	14000 s	41000 s	15000 s	43000 s	27000 s
ReachSafety-Sequentialized 91 tasks		73		80	71	53	28	1	1	10	46	48	80	57
CPU time		74000 s		82000 s	31000 s	71000 s	15000 s	82000 s	82000 s	82000 s	32000 s	25000 s	82000 s	35000 s
ReachSafety-XCSP 114 tasks		114		105	105	114	101	2	73	101	107	90	106	76
CPU time		5600 s		100000 s	40000 s	5800 s	17000 s	100000 s	100000 s	100000 s	77000 s	16000 s	100000 s	16000 s
ReachSafety-Combinations 671 tasks		233		340	305	167	197	182	219	79	285	277	252	152
CPU time		550000 s		600000 s	490000 s	500000 s	470000 s	530000 s	580000 s	600000 s	500000 s	360000 s	600000 s	520000 s
SoftwareSystems-BusyBox-MemSafety 62 tasks		10		21	1	5	18	0	0	13	12	14	0	0
CPU time		55000 s		52000 s	430 s	42000 s	50000 s	56000 s	56000 s	54000 s	34000 s	27000 s	56000 s	610 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety 287 tasks		59		59	59	6	24	54	53	16	42	56	56	0
CPU time		36000 s		260000 s	250000 s	24000 s	59000 s	260000 s	260000 s	240000 s	230000 s	20000 s	260000 s	1600 s
SoftwareSystems-SQLite-MemSafety 1 tasks		0		0	0	0	0	0	0	0	0	0	0	0
CPU time		900 s		900 s	0.35 s	900 s	28 s	900 s	810 s	900 s	3.0 s	46 s	900 s	170 s
Termination-MainHeap 32 tasks		31		30	30	27	16	23	27	11	29	31	29	29
CPU time		7600 s		29000 s	17000 s	7200 s	53 s	26000 s	22000 s	11000 s	27000 s	10000 s	27000 s	23000 s
Overall 4106 tasks		2073		2813	2666	1629	1961		1329	927	2128		2673	1770
CPU time		1800000 s		2800000 s	1800000 s	1900000 s	1000000 s		2500000 s	2600000 s	1600000 s		2600000 s	1100000 s
Participants	Plots	CoVeriTest	ESBMC-kind	FuSeBMC	FuSeBMC_IA	HybridTiger	KLEE	Legion	Legion/SymCC	PRTest	Symbiotic	TracerX	VeriFuzz	WASP-C

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