FASE 2020
2nd Competition on Software Testing (Test-Comp 2020)

Results of the Competition

This web page presents the results of Test-Comp 2020 - 2nd International Competition on Software Testing.

• Competition Definition
• Competition Report for Test-Comp 2020
• 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 2020 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. VeriFuzz 2. LibKluzzer 3. ESBMC	Cover-Branches 1. LibKluzzer 2. VeriFuzz 3. CoVeriTest	Overall 1. VeriFuzz 2. LibKluzzer 3. KLEE

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 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	HybridTiger	KLEE	Legion	LibKluzzer	PRTest	Symbiotic	Tracer-X	VeriFuzz
Representing Jury Member		Marie-Christine Jakobs	Lucas Cordeiro	Sebastian Ruland	Martin Nowack	Gidon Ernst	Hoang M. Le	Thomas Lemberger	Marek Chalupa	Joxan Jaffar	Raveendra Kumar Medicherla
Affiliation		TU Darmstadt	University of Manchester	TU Darmstadt	Imperial College London	LMU Munich	University of Bremen	LMU Munich	Masaryk University, Brno	National University of Singapore, Singapore	Tata Consultancy Service Ltd
Cover-Error 699 tasks		405	506	394	502	302	630	66	435	373	636
CPU time		49000 s	34000 s	36000 s	17000 s	4300 s	470000 s	23000 s	22000 s	25000 s	63000 s
coverage-error-call.ReachSafety-Arrays 30 tasks		1	7	1	7	24	26	6	5	7	24
CPU time		25 s	180 s	6.2 s	1.6 s	850 s	23000 s	4500 s	600 s	68 s	110 s
coverage-error-call.ReachSafety-BitVectors 10 tasks		7	8	7	9	5	10	0	9	9	10
CPU time		180 s	3.8 s	120 s	1.8 s	220 s	9000 s	0 s	930 s	190 s	620 s
coverage-error-call.ReachSafety-ControlFlow 8 tasks		8	5	8	8	0	8	0	8	8	7
CPU time		86 s	3.1 s	96 s	1.6 s	0 s	7200 s	0 s	1400 s	1.3 s	580 s
coverage-error-call.ReachSafety-ECA 412 tasks		183	254	206	259	0	288	0	266	75	376
CPU time		32000 s	32000 s	20000 s	12000 s	0 s	260000 s	0 s	17000 s	19000 s	53000 s
coverage-error-call.ReachSafety-Floats 32 tasks		25	30	24	1	11	29	3	0	0	29
CPU time		3200 s	980 s	3300 s	.14 s	1900 s	26000 s	2700 s	0 s	0 s	780 s
coverage-error-call.ReachSafety-Heap 54 tasks		41	38	39	50	46	51	12	51	48	50
CPU time		7900 s	120 s	3200 s	8.1 s	490 s	33000 s	8200 s	110 s	1900 s	320 s
coverage-error-call.ReachSafety-Loops 30 tasks		22	23	22	25	25	28	8	24	22	27
CPU time		370 s	19 s	210 s	5.2 s	680 s	21000 s	7200 s	430 s	21 s	730 s
coverage-error-call.ReachSafety-Recursive 16 tasks		3	16	1	16	9	16	1	16	10	15
CPU time		15 s	350 s	5.1 s	2.6 s	180 s	14000 s	900 s	87 s	1200 s	1500 s
coverage-error-call.ReachSafety-Sequentialized 107 tasks		61	89	61	98	0	81	0	16	25	100
CPU time		5300 s	840 s	9200 s	4800 s	0 s	73000 s	0 s	2000 s	2800 s	4800 s
Cover-Branches 2531 tasks		1412		1351	1342	1257	1597	545	849	1244	1577
CPU time		1500000 s		1500000 s	1700000 s	570000 s	1900000 s	1800000 s	120000 s	1100000 s	2100000 s
coverage-branches.ReachSafety-Arrays 243 tasks		123		126	121	193	201	93	75	116	200
CPU time		210000 s		200000 s	120000 s	56000 s	150000 s	150000 s	80000 s	120000 s	220000 s
coverage-branches.ReachSafety-BitVectors 36 tasks		28		27	26	23	28	3	19	28	28
CPU time		18000 s		6600 s	11000 s	12000 s	32000 s	32000 s	14 s	16000 s	32000 s
coverage-branches.ReachSafety-ControlFlow 19 tasks		14		14	13	4	14	1	2	13	13
CPU time		1400 s		1600 s	4.8 s	13000 s	17000 s	17000 s	6.9 s	81 s	17000 s
coverage-branches.ReachSafety-ECA 1046 tasks		811		766	957	646	962	489	639	932	963
CPU time		900000 s		940000 s	940000 s	280000 s	940000 s	940000 s	21000 s	660000 s	940000 s
coverage-branches.ReachSafety-Floats 212 tasks		107		107	60	106	107	51	56	51	98
CPU time		84000 s		75000 s	27000 s	60000 s	190000 s	190000 s	17000 s	13000 s	190000 s
coverage-branches.ReachSafety-Heap 139 tasks		92		98	101	103	104	52	83	95	103
CPU time		73000 s		56000 s	76000 s	21000 s	110000 s	77000 s	1700 s	38000 s	120000 s
coverage-branches.ReachSafety-Loops 123 tasks		96		93	93	94	101	54	71	87	97
CPU time		64000 s		64000 s	54000 s	30000 s	100000 s	99000 s	1800 s	45000 s	110000 s
coverage-branches.ReachSafety-Recursive 38 tasks		31		31	32	33	34	10	21	28	34
CPU time		18000 s		4100 s	24000 s	5200 s	34000 s	9900 s	9.7 s	14000 s	34000 s
coverage-branches.ReachSafety-Sequentialized 81 tasks		57		43	53	31	58	5	14	16	62
CPU time		60000 s		65000 s	36000 s	31000 s	73000 s	73000 s	550 s	25000 s	73000 s
coverage-branches.SoftwareSystems-BusyBox-MemSafety 72 tasks		10		4	5	0	21	13	2	14	19
CPU time		64000 s		60000 s	62000 s	3300 s	61000 s	61000 s	41 s	49000 s	65000 s
coverage-branches.SoftwareSystems-DeviceDriversLinux64-ReachSafety 290 tasks		23		22	22	23	22	9	21	22	23
CPU time		31000 s		31000 s	250000 s	17000 s	100000 s	110000 s	110 s	35000 s	110000 s
coverage-branches.SoftwareSystems-SQLite-MemSafety 1 tasks		0		0	0	0	0	0	0	0	0
CPU time		21 s		23 s	900 s	23 s	130 s	900 s	23 s	7.7 s	900 s
coverage-branches.Termination-MainHeap 231 tasks		181		180	153	189	195	53	129	175	195
CPU time		23000 s		16000 s	48000 s	34000 s	120000 s	68000 s	2600 s	63000 s	210000 s
Overall 3230 tasks		1836		1772	2017	1501	2474	500	1548	1654	2476
CPU time		1600000 s		1600000 s	1700000 s	570000 s	2400000 s	1900000 s	150000 s	1100000 s	2200000 s
Participants	Plots	CoVeriTest	ESBMC	HybridTiger	KLEE	Legion	LibKluzzer	PRTest	Symbiotic	Tracer-X	VeriFuzz

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