ETAPS Logo TACAS 2024
13th Competition on Software Verification (SV-COMP 2024)

Results of the Competition on Witness Validation

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

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:


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 (w2.0)
2. Mopsa (w2.0)
3. CPAchecker (w2.0)
MemSafety
1. UAutomizer (w2.0)
2. Mopsa (w2.0)
3. Goblint (w2.0)
ConcurrencySafety
1. –
2. –
3. –
NoOverflows
1. UAutomizer (w2.0)
2. Mopsa (w2.0)
3. Goblint (w2.0)
Termination
1. –
2. –
3. –
SoftwareSystems
1. Mopsa (w2.0)
2. Goblint (w2.0)
3. UAutomizer (w2.0)
Overall
1. UAutomizer (w2.0)
2. Mopsa (w2.0)
3. Goblint (w2.0)

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.

ParticipantsPlotsCPAchecker (w2.0)Goblint (w2.0)Mopsa (w2.0)UAutomizer (w2.0)
Representing Jury MemberDaniel BaierSimmo SaanRaphaël MonatMatthias Heizmann
AffiliationLMU Munich, GermanyUniversity of Tartu, EstoniaInria and University of Lille, FranceUniversity of Freiburg, Germany
ReachSafety
5944 valid tasks (4237 correct, 1707 wrong, 80298 void), max. score: 7133
2872244432844545
CPU time84000 s1100 s60000 s250000 s
ReachSafety-Arrays
45 valid tasks (13 correct, 32 wrong, 2004 void), max. score: 67
24243848
CPU time67 s1.4 s13 s470 s
ReachSafety-BitVectors
45 valid tasks (38 correct, 7 wrong, 552 void), max. score: 68
34384545
CPU time230 s3.5 s57 s1200 s
ReachSafety-ControlFlow
99 valid tasks (41 correct, 58 wrong, 380 void), max. score: 148
8513999
CPU time310 s490 s120 s1800 s
ReachSafety-ECA
791 valid tasks (619 correct, 172 wrong, 5557 void), max. score: 1187
78804871
CPU time32000 s0 s14 s70000 s
ReachSafety-Floats
1053 valid tasks (603 correct, 450 wrong, 8531 void), max. score: 1580
9922263231038
CPU time6600 s16 s270 s64000 s
ReachSafety-Heap
513 valid tasks (495 correct, 18 wrong, 2186 void), max. score: 770
406394475551
CPU time3600 s83 s650 s16000 s
ReachSafety-Loops
941 valid tasks (807 correct, 134 wrong, 9271 void), max. score: 1412
4705107931026
CPU time8800 s150 s3400 s31000 s
ReachSafety-ProductLines
956 valid tasks (956 correct, 0 wrong, 4041 void), max. score: 956
254575956781
CPU time12000 s220 s39000 s26000 s
ReachSafety-Recursive
94 valid tasks (71 correct, 23 wrong, 1203 void), max. score: 141
23944896
CPU time120 s11 s43 s6100 s
ReachSafety-Sequentialized
164 valid tasks (9 correct, 155 wrong, 1792 void), max. score: 246
18129146167
CPU time300 s8.5 s10 s3200 s
ReachSafety-XCSP
20 valid tasks (0 correct, 20 wrong, 1024 void), max. score: 10
0000
CPU time140 s0 s0 s0 s
ReachSafety-Combinations
102 valid tasks (0 correct, 102 wrong, 1708 void), max. score: 51
0000
CPU time0 s0 s0 s360 s
ReachSafety-Hardware
677 valid tasks (141 correct, 536 wrong, 3492 void), max. score: 1016
182471615610
CPU time420 s150 s180 s13000 s
ReachSafety-Hardness
444 valid tasks (444 correct, 0 wrong, 38542 void), max. score: 444
42277297175
CPU time19000 s18 s16000 s15000 s
ReachSafety-Fuzzle
0 valid tasks (0 correct, 0 wrong, 15 void)
0000
CPU time0 s0 s0 s0 s
MemSafety
6405 valid tasks (6112 correct, 293 wrong, 23258 void), max. score: 8006
422550155213
CPU time940 s9100 s690000 s
MemSafety-Arrays
384 valid tasks (264 correct, 120 wrong, 1562 void), max. score: 576
384384384
CPU time51 s310 s6400 s
MemSafety-Heap
144 valid tasks (82 correct, 62 wrong, 1033 void), max. score: 216
102112144
CPU time6.7 s750 s2900 s
MemSafety-LinkedLists
36 valid tasks (12 correct, 24 wrong, 1210 void), max. score: 54
153636
CPU time0.60 s23 s2400 s
MemSafety-Other
355 valid tasks (289 correct, 66 wrong, 986 void), max. score: 533
321354339
CPU time42 s380 s8000 s
MemSafety-Juliet
5465 valid tasks (5465 correct, 0 wrong, 18074 void), max. score: 5465
508950305068
CPU time840 s7700 s670000 s
MemSafety-MemCleanup
21 valid tasks (0 correct, 21 wrong, 393 void), max. score: 11
000
CPU time0 s0 s0 s
ConcurrencySafety
557 valid tasks (0 correct, 557 wrong, 25733 void), max. score: 278
0
CPU time0 s
ConcurrencySafety-Main
271 valid tasks (0 correct, 271 wrong, 3796 void), max. score: 135
0
CPU time0 s
ConcurrencySafety-MemSafety
45 valid tasks (0 correct, 45 wrong, 7388 void), max. score: 23
0
CPU time0 s
ConcurrencySafety-NoOverflows
19 valid tasks (0 correct, 19 wrong, 8535 void), max. score: 9
0
CPU time0 s
NoDataRace-Main
222 valid tasks (0 correct, 222 wrong, 6014 void), max. score: 111
0
CPU time0 s
NoOverflows
25439 valid tasks (17914 correct, 7525 wrong, 49880 void), max. score: 38158
16933171432360125441
CPU time150000 s2800 s28000 s780000 s
NoOverflows-Main
4781 valid tasks (4020 correct, 761 wrong, 16068 void), max. score: 7172
3466222840904782
CPU time55000 s440 s7400 s160000 s
NoOverflows-Juliet
20658 valid tasks (13894 correct, 6764 wrong, 33812 void), max. score: 30987
12524182172065820658
CPU time93000 s2300 s21000 s620000 s
Termination
2 valid tasks (0 correct, 2 wrong, 9178 void)
0
CPU time0 s
Termination-BitVectors
0 valid tasks (0 correct, 0 wrong, 131 void)
0
CPU time0 s
Termination-MainControlFlow
0 valid tasks (0 correct, 0 wrong, 749 void)
0
CPU time0 s
Termination-MainHeap
0 valid tasks (0 correct, 0 wrong, 319 void)
0
CPU time0 s
Termination-Other
2 valid tasks (0 correct, 2 wrong, 7979 void), max. score: 1
0
CPU time0 s
SoftwareSystems
7267 valid tasks (6137 correct, 1130 wrong, 26325 void), max. score: 5450
1097279335211258
CPU time53000 s33000 s81000 s320000 s
SoftwareSystems-AWS-C-Common-ReachSafety
376 valid tasks (98 correct, 278 wrong, 3145 void), max. score: 564
27131830738
CPU time2100 s34 s110 s9600 s
SoftwareSystems-coreutils-MemSafety
0 valid tasks (0 correct, 0 wrong, 160 void)
000
CPU time0 s0 s0 s
SoftwareSystems-coreutils-NoOverflows
0 valid tasks (0 correct, 0 wrong, 124 void)
0000
CPU time0 s0 s0 s0 s
SoftwareSystems-BusyBox-NoOverflows
126 valid tasks (8 correct, 118 wrong, 309 void), max. score: 189
940126126
CPU time4300 s0 s10 s400 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety
6355 valid tasks (5997 correct, 358 wrong, 16174 void), max. score: 9533
2173487463376208
CPU time46000 s33000 s78000 s310000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety
0 valid tasks (0 correct, 0 wrong, 22 void)
0000
CPU time0 s0 s0 s0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety
191 valid tasks (8 correct, 183 wrong, 166 void), max. score: 286
1911910
CPU time3.5 s14 s0 s
SoftwareSystems-Other-ReachSafety
8 valid tasks (8 correct, 0 wrong, 182 void), max. score: 8
0880
CPU time0 s110 s2700 s0 s
SoftwareSystems-Other-MemSafety
75 valid tasks (0 correct, 75 wrong, 314 void), max. score: 37
000
CPU time0 s0 s0 s
SoftwareSystems-uthash-ReachSafety
0 valid tasks (0 correct, 0 wrong, 2165 void)
0000
CPU time0 s0 s0 s0 s
SoftwareSystems-uthash-MemSafety
118 valid tasks (0 correct, 118 wrong, 1580 void), max. score: 59
000
CPU time0 s0 s0 s
SoftwareSystems-uthash-NoOverflows
18 valid tasks (18 correct, 0 wrong, 1984 void), max. score: 18
018180
CPU time0 s32 s37 s0 s
Overall
45614 valid tasks (34400 correct, 11214 wrong, 214672 void), max. score: 40482
9881161862088920919
CPU time280000 s38000 s180000 s2000000 s
ParticipantsPlotsCPAchecker (w2.0)Goblint (w2.0)Mopsa (w2.0)UAutomizer (w2.0)

2. Validation of Violation Witnesses (Version 2.0)


Ranking by Category (with Score-Based Quantile Plots)

Validation of violation witnesses was a demonstration category in SV-COMP 2024.


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.

ParticipantsPlotsCPAchecker (w2.0)Witch (w2.0)
Representing Jury MemberDaniel BaierPaulína Ayaziová
AffiliationLMU Munich, GermanyMasaryk University, Brno, Czechia
ReachSafety
10491 valid tasks (275 correct, 10216 wrong, 44249 void), max. score: 12841
31473148
CPU time5100 s2100 s
ReachSafety-Arrays
640 valid tasks (44 correct, 596 wrong, 1969 void), max. score: 960
320320
CPU time440 s23 s
ReachSafety-BitVectors
78 valid tasks (8 correct, 70 wrong, 339 void), max. score: 116
3939
CPU time72 s79 s
ReachSafety-ControlFlow
151 valid tasks (10 correct, 141 wrong, 378 void), max. score: 226
7575
CPU time74 s11 s
ReachSafety-ECA
977 valid tasks (0 correct, 977 wrong, 6398 void), max. score: 977
00
CPU time0 s0 s
ReachSafety-Floats
1082 valid tasks (0 correct, 1082 wrong, 2528 void), max. score: 1082
0
CPU time0 s
ReachSafety-Heap
191 valid tasks (31 correct, 160 wrong, 1475 void), max. score: 286
9595
CPU time380 s42 s
ReachSafety-Loops
1107 valid tasks (37 correct, 1070 wrong, 5105 void), max. score: 1660
553555
CPU time580 s120 s
ReachSafety-ProductLines
729 valid tasks (62 correct, 667 wrong, 4806 void), max. score: 1089
364364
CPU time1700 s1600 s
ReachSafety-Recursive
283 valid tasks (35 correct, 248 wrong, 1179 void), max. score: 425
142142
CPU time480 s13 s
ReachSafety-Sequentialized
277 valid tasks (38 correct, 239 wrong, 4754 void), max. score: 387
138138
CPU time1200 s210 s
ReachSafety-XCSP
69 valid tasks (0 correct, 69 wrong, 1155 void), max. score: 69
00
CPU time0 s0 s
ReachSafety-Combinations
446 valid tasks (10 correct, 436 wrong, 5386 void), max. score: 669
223223
CPU time110 s19 s
ReachSafety-Hardware
517 valid tasks (0 correct, 517 wrong, 4486 void), max. score: 508
00
CPU time0 s0 s
ReachSafety-Hardness
3944 valid tasks (0 correct, 3944 wrong, 4133 void), max. score: 3944
00
CPU time0 s0 s
ReachSafety-Fuzzle
0 valid tasks (0 correct, 0 wrong, 158 void)
00
CPU time0 s0 s
MemSafety
34 valid tasks (0 correct, 34 wrong, 5464 void), max. score: 28
0
CPU time0 s
MemSafety-Arrays
8 valid tasks (0 correct, 8 wrong, 551 void), max. score: 8
0
CPU time0 s
MemSafety-Heap
7 valid tasks (0 correct, 7 wrong, 1364 void), max. score: 7
0
CPU time0 s
MemSafety-LinkedLists
1 valid tasks (0 correct, 1 wrong, 859 void), max. score: 1
0
CPU time0 s
MemSafety-Other
17 valid tasks (0 correct, 17 wrong, 439 void), max. score: 17
0
CPU time0 s
MemSafety-Juliet
0 valid tasks (0 correct, 0 wrong, 1414 void)
0
CPU time0 s
MemSafety-MemCleanup
1 valid tasks (0 correct, 1 wrong, 837 void), max. score: 1
0
CPU time0 s
ConcurrencySafety
6838 valid tasks (0 correct, 6838 wrong, 11357 void), max. score: 6838
0
CPU time0 s
ConcurrencySafety-Main
1255 valid tasks (0 correct, 1255 wrong, 5905 void), max. score: 1255
0
CPU time0 s
ConcurrencySafety-MemSafety
1913 valid tasks (0 correct, 1913 wrong, 1410 void), max. score: 1913
0
CPU time0 s
ConcurrencySafety-NoOverflows
1880 valid tasks (0 correct, 1880 wrong, 1417 void), max. score: 1880
0
CPU time0 s
NoDataRace-Main
1790 valid tasks (0 correct, 1790 wrong, 2625 void), max. score: 1790
0
CPU time0 s
NoOverflows
6193 valid tasks (0 correct, 6193 wrong, 40699 void), max. score: 6193
0-17
CPU time0 s0 s
NoOverflows-Main
1476 valid tasks (0 correct, 1476 wrong, 8790 void), max. score: 1476
0-8
CPU time0 s0 s
NoOverflows-Juliet
4717 valid tasks (0 correct, 4717 wrong, 31909 void), max. score: 4717
00
CPU time0 s0 s
Termination
41 valid tasks (0 correct, 41 wrong, 8711 void), max. score: 41
0
CPU time0 s
Termination-BitVectors
8 valid tasks (0 correct, 8 wrong, 136 void), max. score: 8
0
CPU time0 s
Termination-MainControlFlow
17 valid tasks (0 correct, 17 wrong, 747 void), max. score: 17
0
CPU time0 s
Termination-MainHeap
1 valid tasks (0 correct, 1 wrong, 222 void), max. score: 1
0
CPU time0 s
Termination-Other
15 valid tasks (0 correct, 15 wrong, 7606 void), max. score: 15
0
CPU time0 s
SoftwareSystems
3964 valid tasks (30 correct, 3934 wrong, 12271 void), max. score: 3799
165165
CPU time590 s190 s
SoftwareSystems-AWS-C-Common-ReachSafety
187 valid tasks (30 correct, 157 wrong, 3066 void), max. score: 281
9393
CPU time590 s190 s
SoftwareSystems-coreutils-MemSafety
169 valid tasks (0 correct, 169 wrong, 570 void), max. score: 169
0
CPU time0 s
SoftwareSystems-coreutils-NoOverflows
115 valid tasks (0 correct, 115 wrong, 30 void), max. score: 115
00
CPU time0 s0 s
SoftwareSystems-BusyBox-NoOverflows
30 valid tasks (0 correct, 30 wrong, 293 void), max. score: 30
00
CPU time0 s0 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety
2939 valid tasks (0 correct, 2939 wrong, 3572 void), max. score: 2939
00
CPU time0 s0 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety
6 valid tasks (0 correct, 6 wrong, 8 void), max. score: 6
00
CPU time0 s0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety
4 valid tasks (0 correct, 4 wrong, 1040 void), max. score: 4
0
CPU time0 s
SoftwareSystems-Other-ReachSafety
93 valid tasks (0 correct, 93 wrong, 154 void), max. score: 93
00
CPU time0 s0 s
SoftwareSystems-Other-MemSafety
22 valid tasks (0 correct, 22 wrong, 288 void), max. score: 22
0
CPU time0 s
SoftwareSystems-uthash-ReachSafety
196 valid tasks (0 correct, 196 wrong, 894 void), max. score: 196
00
CPU time0 s0 s
SoftwareSystems-uthash-MemSafety
0 valid tasks (0 correct, 0 wrong, 1570 void)
0
CPU time0 s
SoftwareSystems-uthash-NoOverflows
203 valid tasks (0 correct, 203 wrong, 786 void), max. score: 203
00
CPU time0 s0 s
Overall
27561 valid tasks (305 correct, 27256 wrong, 122751 void), max. score: 27633
15691557
CPU time5700 s2300 s
ParticipantsPlotsCPAchecker (w2.0)Witch (w2.0)

3. Validation of Correctness Witnesses (Version 1.0)


Ranking by Category (with Score-Based Quantile Plots)

ReachSafety
1. UAutomizer (w1.0)
2. CPAchecker (w1.0)
3. LIV (w1.0)
MemSafety
1. UAutomizer (w1.0)
2. LIV (w1.0)
3. MetaVal (w1.0)
ConcurrencySafety
1. UAutomizer (w1.0)
2. –
3. –
NoOverflows
1. CPAchecker (w1.0)
2. UAutomizer (w1.0)
3. MetaVal (w1.0)
Termination
1. –
2. –
3. –
SoftwareSystems
1. CPAchecker (w1.0)
2. UAutomizer (w1.0)
3. LIV (w1.0)
Overall
1. UAutomizer (w1.0)
2. CPAchecker (w1.0)
3. MetaVal (w1.0)

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.

ParticipantsPlotsCPAchecker (w1.0)JCWIT (w1.0)LIV (w1.0)MetaVal (w1.0)UAutomizer (w1.0)
Representing Jury MemberDaniel BaierZaiyu ChengMartin SpiesslMartin SpiesslMatthias Heizmann
AffiliationLMU Munich, GermanyUniversity of Manchester, UKLMU Munich, GermanyLMU Munich, GermanyUniversity of Freiburg, Germany
ReachSafety
35827 valid tasks (33930 correct, 1897 wrong, 50415 void), max. score: 51717
25183-44060-4534628020
CPU time890000 s13000 s3000000 s2000000 s
ReachSafety-Arrays
202 valid tasks (36 correct, 166 wrong, 1847 void), max. score: 385
2020197217
CPU time360 s0 s4100 s2900 s
ReachSafety-BitVectors
410 valid tasks (401 correct, 9 wrong, 187 void), max. score: 661
38936476388
CPU time15000 s150 s50000 s23000 s
ReachSafety-ControlFlow
261 valid tasks (202 correct, 59 wrong, 218 void), max. score: 394
2680-3728252
CPU time2700 s0 s3500 s5400 s
ReachSafety-ECA
2811 valid tasks (2639 correct, 172 wrong, 3537 void), max. score: 4216
27940193161
CPU time230000 s0 s4000 s240000 s
ReachSafety-Floats
6249 valid tasks (5798 correct, 451 wrong, 3335 void), max. score: 9380
6251188-214705647
CPU time90000 s2600 s190000 s700000 s
ReachSafety-Heap
1986 valid tasks (1967 correct, 19 wrong, 713 void), max. score: 3031
1973334-9032286
CPU time25000 s1400 s55000 s63000 s
ReachSafety-Loops
5553 valid tasks (5403 correct, 150 wrong, 4659 void), max. score: 8626
3687-128950835575
CPU time130000 s3400 s400000 s290000 s
ReachSafety-ProductLines
2757 valid tasks (2757 correct, 0 wrong, 2240 void), max. score: 2757
754025202721
CPU time12000 s0 s490000 s95000 s
ReachSafety-Recursive
780 valid tasks (757 correct, 23 wrong, 517 void), max. score: 1170
64-3089-6828795
CPU time380 s780 s8200 s76000 s
ReachSafety-Sequentialized
336 valid tasks (166 correct, 170 wrong, 1620 void), max. score: 519
2570328102
CPU time9900 s0 s44000 s9900 s
ReachSafety-XCSP
834 valid tasks (814 correct, 20 wrong, 210 void), max. score: 1251
876-125107960
CPU time20000 s4500 s29000 s0 s
ReachSafety-Combinations
144 valid tasks (41 correct, 103 wrong, 1666 void), max. score: 217
40150152
CPU time490 s0 s14000 s6000 s
ReachSafety-Hardware
806 valid tasks (270 correct, 536 wrong, 3363 void), max. score: 1209
5823700802
CPU time2100 s630 s0 s19000 s
ReachSafety-Hardness
12698 valid tasks (12679 correct, 19 wrong, 26288 void), max. score: 25396
126970126582606
CPU time350000 s0 s1700000 s430000 s
ReachSafety-Fuzzle
0 valid tasks (0 correct, 0 wrong, 15 void)
0000
CPU time0 s0 s0 s0 s
MemSafety
479 valid tasks (186 correct, 293 wrong, 29184 void), max. score: 359
870259
CPU time780 s0 s17000 s
MemSafety-Arrays
138 valid tasks (18 correct, 120 wrong, 1808 void), max. score: 207
460197
CPU time76 s0 s8400 s
MemSafety-Heap
62 valid tasks (0 correct, 62 wrong, 1115 void), max. score: 31
006
CPU time0 s0 s2600 s
MemSafety-LinkedLists
24 valid tasks (0 correct, 24 wrong, 1222 void), max. score: 12
002
CPU time0 s0 s120 s
MemSafety-Other
234 valid tasks (168 correct, 66 wrong, 1107 void), max. score: 351
1770324
CPU time710 s0 s5300 s
MemSafety-Juliet
0 valid tasks (0 correct, 0 wrong, 23539 void)
000
CPU time0 s0 s0 s
MemSafety-MemCleanup
21 valid tasks (0 correct, 21 wrong, 393 void), max. score: 11
005
CPU time0 s0 s1000 s
ConcurrencySafety
335 valid tasks (0 correct, 335 wrong, 19719 void), max. score: 126
70
CPU time9400 s
ConcurrencySafety-Main
271 valid tasks (0 correct, 271 wrong, 3796 void), max. score: 135
43
CPU time8100 s
ConcurrencySafety-MemSafety
45 valid tasks (0 correct, 45 wrong, 7388 void), max. score: 23
8
CPU time830 s
ConcurrencySafety-NoOverflows
19 valid tasks (0 correct, 19 wrong, 8535 void), max. score: 9
9
CPU time450 s
NoOverflows
49083 valid tasks (41431 correct, 7652 wrong, 26236 void), max. score: 75379
57309-45163056467
CPU time620000 s14000 s0 s1200000 s
NoOverflows-Main
11649 valid tasks (10761 correct, 888 wrong, 9200 void), max. score: 18307
11703-21438015154
CPU time200000 s14000 s0 s410000 s
NoOverflows-Juliet
37434 valid tasks (30670 correct, 6764 wrong, 17036 void), max. score: 56151
498060037434
CPU time420000 s0 s0 s740000 s
Termination
0 valid tasks (0 correct, 0 wrong, 0 void)
CPU time
SoftwareSystems
15274 valid tasks (14128 correct, 1146 wrong, 18318 void), max. score: 7664
32750-153042211
CPU time100000 s0 s1700000 s870000 s
SoftwareSystems-AWS-C-Common-ReachSafety
668 valid tasks (390 correct, 278 wrong, 2853 void), max. score: 1002
6140-2078-173
CPU time11000 s0 s24000 s34000 s
SoftwareSystems-coreutils-MemSafety
0 valid tasks (0 correct, 0 wrong, 160 void)
000
CPU time0 s0 s0 s
SoftwareSystems-coreutils-NoOverflows
0 valid tasks (0 correct, 0 wrong, 124 void)
0000
CPU time0 s0 s0 s0 s
SoftwareSystems-BusyBox-NoOverflows
125 valid tasks (7 correct, 118 wrong, 310 void), max. score: 187
15800125
CPU time8900 s0 s0 s510 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety
14105 valid tasks (13731 correct, 374 wrong, 8424 void), max. score: 21459
55180-12572614019
CPU time80000 s0 s1700000 s830000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety
0 valid tasks (0 correct, 0 wrong, 22 void)
0000
CPU time0 s0 s0 s0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety
183 valid tasks (0 correct, 183 wrong, 174 void), max. score: 92
000
CPU time0 s0 s72 s
SoftwareSystems-Other-ReachSafety
0 valid tasks (0 correct, 0 wrong, 190 void)
0000
CPU time0 s0 s0 s0 s
SoftwareSystems-Other-MemSafety
75 valid tasks (0 correct, 75 wrong, 314 void), max. score: 37
000
CPU time0 s0 s0 s
SoftwareSystems-uthash-ReachSafety
0 valid tasks (0 correct, 0 wrong, 2165 void)
0000
CPU time0 s0 s0 s0 s
SoftwareSystems-uthash-MemSafety
118 valid tasks (0 correct, 118 wrong, 1580 void), max. score: 59
000
CPU time0 s0 s0 s
SoftwareSystems-uthash-NoOverflows
0 valid tasks (0 correct, 0 wrong, 2002 void)
0000
CPU time0 s0 s0 s0 s
Overall
100998 valid tasks (89675 correct, 11323 wrong, 143872 void), max. score: 77534
35095-3817247571
CPU time1600000 s4600000 s4000000 s
ParticipantsPlotsCPAchecker (w1.0)JCWIT (w1.0)LIV (w1.0)MetaVal (w1.0)UAutomizer (w1.0)

4. Validation of Violation Witnesses (Version 1.0)


Ranking by Category (with Score-Based Quantile Plots)

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

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.

ParticipantsPlotsConcurrentWitness2Test (w1.0)CPAchecker (w1.0)CPA-witness2test (w1.0)Dartagnan (w1.0)CProver-witness2test (w1.0)GWIT (w1.0)MetaVal (w1.0)NITWIT (w1.0)Symbiotic-Witch (w1.0)UAutomizer (w1.0)WIT4JAVA (w1.0)
Representing Jury MemberLevente BajcziDaniel BaierThomas LembergerHernán Ponce de LeónHors ConcoursFalk HowarMartin SpiesslJana (Philipp) BergerPaulína AyaziováMatthias HeizmannHors Concours
AffiliationBudapest University of Technology and Economics, HungaryLMU Munich, GermanyLMU Munich, GermanyHuawei Dresden Research Center, Germany--, --TU Dortmund, GermanyLMU Munich, GermanyRWTH Aachen, GermanyMasaryk University, Brno, CzechiaUniversity of Freiburg, Germany--, --
ReachSafety
29189 valid tasks (16947 correct, 12242 wrong, 25551 void), max. score: 38587
0156868188222513984102541382824390
CPU time0 s300000 s130000 s65000 s210000 s7400 s100000 s430000 s
ReachSafety-Arrays
1574 valid tasks (901 correct, 673 wrong, 1035 void), max. score: 2271
66885416873997987461780
CPU time6200 s4600 s1800 s9200 s2900 s2100 s19000 s
ReachSafety-BitVectors
288 valid tasks (201 correct, 87 wrong, 129 void), max. score: 402
284159308145133219303
CPU time2100 s1100 s360 s1900 s2.0 s1100 s4700 s
ReachSafety-ControlFlow
293 valid tasks (133 correct, 160 wrong, 236 void), max. score: 422
193-15327-50620146284
CPU time1400 s440 s380 s1300 s0.20 s450 s3800 s
ReachSafety-ECA
4364 valid tasks (3291 correct, 1073 wrong, 3011 void), max. score: 6351
31281664535323200816854023
CPU time86000 s64000 s32000 s1400 s3200 s28000 s68000 s
ReachSafety-Floats
1634 valid tasks (413 correct, 1221 wrong, 1976 void), max. score: 2358
9236631555-18195966601156
CPU time6300 s2900 s1800 s14000 s4.4 s150 s33000 s
ReachSafety-Heap
1145 valid tasks (915 correct, 230 wrong, 521 void), max. score: 1541
5767451283102830310051184
CPU time7700 s3900 s1600 s16000 s5.6 s870 s17000 s
ReachSafety-Loops
3026 valid tasks (1742 correct, 1284 wrong, 3186 void), max. score: 4286
2109140030732069137126773335
CPU time19000 s8100 s3500 s33000 s21 s6500 s39000 s
ReachSafety-ProductLines
3901 valid tasks (3187 correct, 714 wrong, 1634 void), max. score: 5701
509402888761181520734285
CPU time41000 s0 s7000 s32000 s63 s29000 s44000 s
ReachSafety-Recursive
512 valid tasks (205 correct, 307 wrong, 950 void), max. score: 719
-475291609424248366603
CPU time3100 s1700 s850 s2800 s94 s520 s8400 s
ReachSafety-Sequentialized
3150 valid tasks (2765 correct, 385 wrong, 1881 void), max. score: 3923
17301100534844145210412151
CPU time46000 s23000 s1600 s39000 s990 s9000 s51000 s
ReachSafety-XCSP
749 valid tasks (582 correct, 167 wrong, 475 void), max. score: 904
62132316441261379335
CPU time21000 s1000 s1300 s17000 s26 s9600 s4000 s
ReachSafety-Combinations
3140 valid tasks (1775 correct, 1365 wrong, 2692 void), max. score: 3641
1505570225631513819291213
CPU time32000 s14000 s10000 s11000 s81 s6500 s41000 s
ReachSafety-Hardware
1377 valid tasks (773 correct, 604 wrong, 3626 void), max. score: 1945
928169573005661016
CPU time22000 s4000 s1500 s0 s0 s6000 s23000 s
ReachSafety-Hardness
3944 valid tasks (0 correct, 3944 wrong, 4133 void), max. score: 3944
303135590263944
CPU time3500 s7.4 s5.4 s26000 s0 s220 s72000 s
ReachSafety-Fuzzle
92 valid tasks (64 correct, 28 wrong, 66 void), max. score: 92
48019394528
CPU time2900 s0 s310 s3400 s57 s13 s790 s
MemSafety
2373 valid tasks (169 correct, 2204 wrong, 3125 void), max. score: 1213
6261394430799472
CPU time13000 s3500 s2700 s0 s2100 s19000 s
MemSafety-Arrays
336 valid tasks (0 correct, 336 wrong, 223 void), max. score: 172
2530760140137
CPU time370 s480 s370 s0 s550 s5900 s
MemSafety-Heap
1183 valid tasks (0 correct, 1183 wrong, 188 void), max. score: 595
407973340394120
CPU time7800 s2100 s1400 s0 s940 s5700 s
MemSafety-LinkedLists
322 valid tasks (0 correct, 322 wrong, 538 void), max. score: 161
1121710801257
CPU time2000 s320 s510 s0 s210 s340 s
MemSafety-Other
344 valid tasks (0 correct, 344 wrong, 112 void), max. score: 181
1174464013082
CPU time1800 s640 s390 s0 s300 s3700 s
MemSafety-Juliet
0 valid tasks (0 correct, 0 wrong, 1414 void)
000000
CPU time0 s0 s0 s0 s0 s0 s
MemSafety-MemCleanup
188 valid tasks (169 correct, 19 wrong, 650 void), max. score: 193
901709480
CPU time1200 s55 s0 s130 s3100 s
ConcurrencySafety
11180 valid tasks (4219 correct, 6961 wrong, 7015 void), max. score: 13891
211091866742
CPU time51000 s130000 s260000 s
ConcurrencySafety-Main
5401 valid tasks (4146 correct, 1255 wrong, 1759 void), max. score: 8102
659230252105021
CPU time1500 s50000 s76000 s200000 s
ConcurrencySafety-MemSafety
2036 valid tasks (0 correct, 2036 wrong, 1287 void), max. score: 1975
01387456
CPU time0 s20000 s17000 s
ConcurrencySafety-NoOverflows
1953 valid tasks (73 correct, 1880 wrong, 1344 void), max. score: 2929
64218482458
CPU time410 s20000 s45000 s
NoDataRace-Main
1790 valid tasks (0 correct, 1790 wrong, 2625 void), max. score: 1790
012430
CPU time0 s17000 s0 s
NoOverflows
21017 valid tasks (10868 correct, 10149 wrong, 25875 void), max. score: 28837
18892112971840001463920030
CPU time290000 s86000 s28000 s0 s45000 s230000 s
NoOverflows-Main
6044 valid tasks (4471 correct, 1573 wrong, 4222 void), max. score: 8880
577916394852050538205
CPU time42000 s13000 s5800 s0 s27000 s100000 s
NoOverflows-Juliet
14973 valid tasks (6397 correct, 8576 wrong, 21653 void), max. score: 19091
126011203714197083408215
CPU time250000 s73000 s22000 s0 s17000 s120000 s
Termination
1077 valid tasks (991 correct, 86 wrong, 7675 void), max. score: 1399
-14960692
CPU time19000 s0 s25000 s
Termination-BitVectors
55 valid tasks (36 correct, 19 wrong, 89 void), max. score: 67
-13251
CPU time240 s800 s
Termination-MainControlFlow
260 valid tasks (228 correct, 32 wrong, 504 void), max. score: 329
-8450146
CPU time1700 s0 s4900 s
Termination-MainHeap
7 valid tasks (6 correct, 1 wrong, 216 void), max. score: 10
303
CPU time99 s0 s120 s
Termination-Other
755 valid tasks (721 correct, 34 wrong, 6866 void), max. score: 922
-3110444
CPU time17000 s0 s20000 s
SoftwareSystems
6741 valid tasks (515 correct, 6226 wrong, 9494 void), max. score: 6232
1359472-119492116962633
CPU time54000 s3900 s2200 s26000 s2100 s93000 s
SoftwareSystems-AWS-C-Common-ReachSafety
545 valid tasks (326 correct, 219 wrong, 2708 void), max. score: 740
35203772980403392
CPU time6000 s0 s1100 s7500 s0 s1000 s6400 s
SoftwareSystems-coreutils-MemSafety
592 valid tasks (0 correct, 592 wrong, 147 void), max. score: 381
0-32-984000
CPU time0 s0 s0 s0 s0 s0 s
SoftwareSystems-coreutils-NoOverflows
115 valid tasks (0 correct, 115 wrong, 30 void), max. score: 115
000000
CPU time0 s0 s0 s0 s0 s0 s
SoftwareSystems-BusyBox-NoOverflows
30 valid tasks (0 correct, 30 wrong, 293 void), max. score: 30
2000030
CPU time74 s0 s0 s0 s0 s810 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety
3296 valid tasks (189 correct, 3107 wrong, 3215 void), max. score: 4855
295934522069052493
CPU time30000 s24 s890 s15000 s0 s8.7 s74000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety
6 valid tasks (0 correct, 6 wrong, 8 void), max. score: 6
0000000
CPU time0 s0 s0 s0 s0 s0 s0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety
902 valid tasks (0 correct, 902 wrong, 142 void), max. score: 453
207658056
CPU time8200 s2100 s49 s0 s31 s510 s
SoftwareSystems-Other-ReachSafety
93 valid tasks (0 correct, 93 wrong, 154 void), max. score: 93
36000000
CPU time2000 s0 s0 s0 s0 s0 s0 s
SoftwareSystems-Other-MemSafety
93 valid tasks (0 correct, 93 wrong, 217 void), max. score: 57
00-1210019
CPU time0 s0 s150 s0 s0 s1100 s
SoftwareSystems-uthash-ReachSafety
196 valid tasks (0 correct, 196 wrong, 894 void), max. score: 196
000910196196
CPU time0 s0 s0 s3700 s0 s210 s4900 s
SoftwareSystems-uthash-MemSafety
670 valid tasks (0 correct, 670 wrong, 900 void), max. score: 335
1290001830
CPU time7800 s0 s0 s0 s590 s0 s
SoftwareSystems-uthash-NoOverflows
203 valid tasks (0 correct, 203 wrong, 786 void), max. score: 203
016700203203
CPU time0 s1700 s0 s0 s260 s5200 s
Overall
71577 valid tasks (33709 correct, 37868 wrong, 78735 void), max. score: 79588
836811295980119651325841912098043235
CPU time730000 s220000 s130000 s97000 s230000 s7400 s150000 s1000000 s
ParticipantsPlotsConcurrentWitness2Test (w1.0)CPAchecker (w1.0)CPA-witness2test (w1.0)Dartagnan (w1.0)CProver-witness2test (w1.0)GWIT (w1.0)MetaVal (w1.0)NITWIT (w1.0)Symbiotic-Witch (w1.0)UAutomizer (w1.0)WIT4JAVA (w1.0)

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

Imprint and Privacy Policy