![]() |
TACAS 2021 |
10th Competition on Software Verification (SV-COMP 2021) |
This web page presents the results of SV-COMP 2021 - 10th 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 reading the score-based quantile plots:
Here some brief directions for navigating in the BenchExec-generated tables with the results:
ReachSafety 1. VeriAbs 2. CPAchecker 3. PeSCo |
MemSafety 1. Symbiotic 2. CPAchecker 3. UAutomizer |
ConcurrencySafety 1. Lazy-CSeq 2. CPAchecker 3. UAutomizer |
NoOverflows 1. CPAchecker 2. UAutomizer 3. UTaipan |
Termination 1. UAutomizer 2. CPAchecker 3. 2LS |
SoftwareSystems 1. Symbiotic 2. SMACK 3. PeSCo |
FalsificationOverall 1. CPAchecker 2. PeSCo 3. UAutomizer |
Overall 1. CPAchecker 2. PeSCo 3. UAutomizer |
|
JavaOverall 1. Java-Ranger 2. JDart 3. JBMC |
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.
Participants | Plots | 2LS | BRICK | CBMC | CPA-BAM-BnB | CPALockator | CPAchecker | Dartagnan | DIVINE | ESBMC-incr | ESBMC-kind | Frama-C | Gazer-Theta | Goblint | Korn | Lazy-CSeq | PeSCo | Pinaka | PredatorHP | SMACK | Symbiotic | UAutomizer | UKojak | UTaipan | VeriAbs | COASTAL | Java-Ranger | JayHorn | JBMC | JDart | SPF |
Representing Jury Member | Viktor Malík | Lei Bu | Michael Tautschnig | Vadim Mutilin | Pavel Andrianov | Stephan Holzner | Hernán Ponce de León | Henrich Lauko | Felipe R. Monteiro | Lucas Cordeiro | Martin Spiessl | Ákos Hajdu | Simmo Saan | Gidon Ernst | Omar Inverso | Cedric Richter | Saurabh Joshi | Hors Concours | Zvonimir Rakamaric | Marek Chalupa | Matthias Heizmann | Dominik Klumpp | Daniel Dietsch | Priyanka Darke | Hors Concours | Soha Hussein | Hossein Hojjat | Peter Schrammel | Falk Howar | Hors Concours | |
Affiliation | TU Brno, Czechia | Nanjing University, China | Queen Mary University of London, UK | ISP RAS, Russia | ISP RAS, Russia | LMU Munich, Germany | University of the Bundeswehr Munich, Germany | Masaryk University Brno, Czechia | Amazon Web Services, USA | University of Manchester, UK | LMU Munich, Germany | Budapest University of Technology and Economics, Hungary | University of Tartu, Estonia | LMU Munich, Germany | Gran Sasso Science Institute, Italy | Paderborn University, Germany | IIT Hyderabad, India | -- | University of Utah, USA | Masaryk University Brno, Czechia | University of Freiburg, Germany | University of Freiburg, Germany | University of Freiburg, Germany | Tata Consultancy Services, India | -- | University of Minnesota, USA | University of Tehran, Iran | University of Sussex and Diffblue, UK | TU Dortmund, Germany | -- | |
ReachSafety 4927 tasks, max. score: 7844 |
3021 | 3395 | 4764 | 2012 | 4486 | 777 | 4526 | 3408 | 3864 | 3502 | 1768 | 2743 | 5771 | ||||||||||||||||||
CPU time | 85000 s | 64000 s | 380000 s | 120000 s | 130000 s | 1500 s | 190000 s | 22000 s | 50000 s | 160000 s | 90000 s | 140000 s | 480000 s | ||||||||||||||||||
unreach-call.ReachSafety-Arrays 436 tasks, max. score: 759 |
-28 | -80 | 78 | 36 | 41 | 150 | 40 | 81 | 125 | 216 | 89 | 82 | 89 | 705 | |||||||||||||||||
CPU time | 100 s | 5300 s | 11000 s | 1700 s | 1900 s | 1100 s | 5.2 s | 4100 s | 2000 s | 2900 s | 1900 s | 1500 s | 4000 s | 12000 s | |||||||||||||||||
unreach-call.ReachSafety-BitVectors 49 tasks, max. score: 83 |
53 | 43 | 71 | 2 | 44 | 57 | 63 | 8 | 57 | 40 | 45 | 48 | 24 | 47 | 74 | ||||||||||||||||
CPU time | 47 s | 380 s | 4300 s | 93 s | 700 s | 340 s | 370 s | 0.29 s | 2700 s | 65 s | 150 s | 2000 s | 210 s | 2500 s | 2900 s | ||||||||||||||||
unreach-call.ReachSafety-ControlFlow 92 tasks, max. score: 142 |
66 | 67 | 127 | -80 | 88 | 59 | 0 | 71 | 137 | 33 | 60 | 92 | 40 | 73 | 103 | ||||||||||||||||
CPU time | 2200 s | 560 s | 10000 s | 1200 s | 3700 s | 32 s | 0 s | 5200 s | 6000 s | 350 s | 550 s | 3700 s | 2800 s | 3700 s | 12000 s | ||||||||||||||||
unreach-call.ReachSafety-ECA 1265 tasks, max. score: 2050 |
600 | 171 | 916 | 144 | 1096 | 392 | 2 | 1019 | 261 | 121 | 596 | 434 | 331 | 1268 | |||||||||||||||||
CPU time | 57000 s | 32000 s | 130000 s | 50000 s | 83000 s | 27000 s | 51 s | 95000 s | 6300 s | 5100 s | 43000 s | 48000 s | 33000 s | 200000 s | |||||||||||||||||
unreach-call.ReachSafety-Floats 469 tasks, max. score: 893 |
633 | 0 | 801 | 747 | 258 | 780 | 337 | 2 | 767 | 801 | 654 | 645 | 2 | 646 | 817 | ||||||||||||||||
CPU time | 1900 s | 0 s | 8500 s | 11000 s | 8000 s | 5400 s | 290 s | 0.095 s | 14000 s | 2300 s | 1300 s | 38000 s | 13 s | 37000 s | 18000 s | ||||||||||||||||
unreach-call.ReachSafety-Heap 241 tasks, max. score: 408 |
139 | 288 | 282 | 201 | 254 | 120 | 284 | 229 | 309 | 252 | 220 | 211 | 295 | ||||||||||||||||||
CPU time | 180 s | 95 s | 4500 s | 810 s | 400 s | 69 s | 5100 s | 12 s | 340 s | 5800 s | 4900 s | 6800 s | 9400 s | ||||||||||||||||||
unreach-call.ReachSafety-Loops 768 tasks, max. score: 1303 |
383 | 581 | 635 | 341 | 675 | 647 | 628 | 76 | 646 | 440 | 709 | 448 | 615 | 354 | -127 | 1015 | |||||||||||||||
CPU time | 6900 s | 10000 s | 18000 s | 5900 s | 18000 s | 19000 s | 8500 s | 840 s | 9600 s | 15000 s | 5100 s | 2300 s | 26000 s | 15000 s | 23000 s | 54000 s | |||||||||||||||
unreach-call.ReachSafety-ProductLines 597 tasks, max. score: 929 |
747 | 298 | 905 | 792 | 783 | 865 | 320 | 849 | 131 | 323 | 612 | 329 | 602 | 860 | |||||||||||||||||
CPU time | 10000 s | 570 s | 80000 s | 16000 s | 610 s | 22000 s | 550 s | 12000 s | 18 s | 1100 s | 17000 s | 7300 s | 17000 s | 96000 s | |||||||||||||||||
unreach-call.ReachSafety-Recursive 105 tasks, max. score: 162 |
0 | 101 | 61 | 110 | 110 | 102 | 52 | 143 | 61 | 95 | 111 | 124 | 85 | 89 | 125 | ||||||||||||||||
CPU time | 0 s | 190 s | 770 s | 1100 s | 890 s | 350 s | 5.8 s | 800 s | 1400 s | 61 s | 160 s | 3200 s | 1800 s | 5200 s | 6800 s | ||||||||||||||||
unreach-call.ReachSafety-Sequentialized 576 tasks, max. score: 762 |
132 | 156 | 462 | -28 | 56 | 2 | 435 | 234 | 319 | 35 | 30 | 61 | 277 | ||||||||||||||||||
CPU time | 4800 s | 3900 s | 98000 s | 20000 s | 1500 s | 0.38 s | 28000 s | 2400 s | 6700 s | 11000 s | 8100 s | 4500 s | 46000 s | ||||||||||||||||||
unreach-call.ReachSafety-XCSP 119 tasks, max. score: 179 |
148 | 157 | 153 | 9 | 158 | 147 | 0 | 92 | 147 | 147 | 144 | 43 | 7 | 49 | 108 | ||||||||||||||||
CPU time | 2100 s | 1200 s | 3800 s | 1800 s | 2300 s | 450 s | 0 s | 750 s | 7500 s | 1900 s | 11000 s | 6000 s | 320 s | 7200 s | 3000 s | ||||||||||||||||
unreach-call.ReachSafety-Combinations 210 tasks, max. score: 270 |
0 | 0 | 20 | 0 | 53 | 0 | 0 | 0 | 60 | 132 | 5 | 0 | 0 | 105 | |||||||||||||||||
CPU time | 0 s | 0 s | 920 s | 0 s | 7400 s | 0 s | 0 s | 0 s | 1400 s | 18000 s | 3900 s | 0 s | 0 s | 22000 s | |||||||||||||||||
MemSafety 3296 tasks, max. score: 4981 |
1100 | -725 | 2992 | 95 | 1281 | 2187 | 3125 | 1615 | 925 | 1436 | |||||||||||||||||||||
CPU time | 350 s | 5400 s | 28000 s | 180 s | 24000 s | 3500 s | 5900 s | 15000 s | 8600 s | 8800 s | |||||||||||||||||||||
valid-memsafety.MemSafety-Arrays 85 tasks, max. score: 145 |
9 | 27 | 5 | 0 | 0 | 5 | 23 | 45 | 62 | 38 | 54 | ||||||||||||||||||||
CPU time | 62 s | 1200 s | 26 s | 0 s | 0 s | 26 s | 60 s | 360 s | 4500 s | 1800 s | 2200 s | ||||||||||||||||||||
valid-memsafety.MemSafety-Heap 184 tasks, max. score: 275 |
70 | 151 | 179 | -58 | 6 | 179 | 215 | 231 | 84 | 69 | 58 | ||||||||||||||||||||
CPU time | 14 s | 1400 s | 1100 s | 110 s | 1500 s | 1100 s | 2900 s | 2300 s | 4700 s | 3000 s | 2800 s | ||||||||||||||||||||
valid-memsafety.MemSafety-LinkedLists 103 tasks, max. score: 178 |
23 | 116 | 114 | 84 | 100 | 114 | 140 | 160 | 10 | 3 | 7 | ||||||||||||||||||||
CPU time | 210 s | 92 s | 790 s | 59 s | 300 s | 820 s | 66 s | 1200 s | 2000 s | 53 s | 1700 s | ||||||||||||||||||||
valid-memsafety.MemSafety-Other 55 tasks, max. score: 87 |
55 | -1 | 52 | -18 | 30 | 52 | 49 | 81 | 63 | 19 | 65 | ||||||||||||||||||||
CPU time | 14 s | 66 s | 410 s | 9.8 s | 3.4 s | 420 s | 500 s | 2000 s | 2200 s | 1600 s | 1400 s | ||||||||||||||||||||
valid-memcleanup.MemSafety-MemCleanup 41 tasks, max. score: 43 |
12 | -188 | 35 | 0 | 0 | 35 | 12 | 36 | 21 | 20 | 17 | ||||||||||||||||||||
CPU time | 54 s | 1.3 s | 260 s | 0 s | 0 s | 260 s | 2.7 s | 32 s | 1400 s | 2100 s | 580 s | ||||||||||||||||||||
valid-memsafety.MemSafety-Juliet 2828 tasks, max. score: 4266 |
0 | 2880 | 4266 | 0 | 2216 | 4266 | 0 | 0 | 0 | 0 | 0 | ||||||||||||||||||||
CPU time | 0 s | 2600 s | 25000 s | 0 s | 22000 s | 26000 s | 0 s | 0 s | 0 s | 0 s | 0 s | ||||||||||||||||||||
ConcurrencySafety 1130 tasks, max. score: 1413 |
0 | 486 | -819 | 1050 | 309 | 391 | -134 | 37 | 46 | 1206 | 0 | 943 | 0 | 937 | |||||||||||||||||
CPU time | 0 s | 2000 s | 260 s | 57000 s | 7700 s | 35000 s | 9500 s | 42000 s | 13 s | 14000 s | 0 s | 35000 s | 0 s | 34000 s | |||||||||||||||||
unreach-call.ConcurrencySafety-Main 1130 tasks, max. score: 1413 |
0 | 486 | -819 | 1050 | 309 | 391 | -134 | 37 | 46 | 1206 | 1050 | 0 | 943 | 0 | 937 | ||||||||||||||||
CPU time | 0 s | 2000 s | 260 s | 57000 s | 7700 s | 35000 s | 9500 s | 42000 s | 13 s | 14000 s | 66000 s | 0 s | 35000 s | 0 s | 34000 s | ||||||||||||||||
NoOverflows 452 tasks, max. score: 682 |
414 | 279 | 531 | 0 | 317 | 172 | 156 | -200 | 373 | 512 | 441 | 506 | |||||||||||||||||||
CPU time | 260 s | 240 s | 4400 s | 0 s | 530 s | 28 s | 7.3 s | 110 s | 2400 s | 6100 s | 5400 s | 7000 s | |||||||||||||||||||
no-overflow.NoOverflows-BitVectors 280 tasks, max. score: 402 |
275 | 186 | 319 | 0 | 189 | 115 | 118 | 319 | 32 | 202 | 338 | 293 | 334 | ||||||||||||||||||
CPU time | 130 s | 71 s | 2100 s | 0 s | 150 s | 19 s | 5.0 s | 2200 s | 11 s | 360 s | 4000 s | 3700 s | 4300 s | ||||||||||||||||||
no-overflow.NoOverflows-Other 172 tasks, max. score: 272 |
146 | 98 | 208 | 0 | 125 | 60 | 46 | 208 | -172 | 160 | 182 | 156 | 180 | ||||||||||||||||||
CPU time | 130 s | 170 s | 2200 s | 0 s | 380 s | 9.7 s | 2.4 s | 2200 s | 98 s | 2100 s | 2100 s | 1700 s | 2700 s | ||||||||||||||||||
Termination 2212 tasks, max. score: 3897 |
1315 | 872 | 1356 | 0 | 832 | 669 | 1043 | 3019 | 0 | 0 | |||||||||||||||||||||
CPU time | 9000 s | 5800 s | 61000 s | 0 s | 3300 s | 1200 s | 13000 s | 80000 s | 0 s | 0 s | |||||||||||||||||||||
termination.Termination-MainControlFlow 250 tasks, max. score: 443 |
272 | 60 | 260 | 0 | 60 | 260 | 54 | -27 | 379 | 0 | 0 | ||||||||||||||||||||
CPU time | 62 s | 46 s | 3100 s | 0 s | 260 s | 3100 s | 10 s | 81 s | 3700 s | 0 s | 0 s | ||||||||||||||||||||
termination.Termination-MainHeap 259 tasks, max. score: 501 |
-26 | 26 | 0 | 0 | 24 | 0 | 56 | 122 | 385 | 0 | 0 | ||||||||||||||||||||
CPU time | 5.4 s | 330 s | 0 s | 0 s | 630 s | 0 s | 160 s | 87 s | 6300 s | 0 s | 0 s | ||||||||||||||||||||
termination.Termination-Other 1703 tasks, max. score: 2689 |
1356 | 1434 | 1361 | 0 | 1356 | 1361 | 808 | 1791 | 1859 | 0 | 0 | ||||||||||||||||||||
CPU time | 8900 s | 5400 s | 58000 s | 0 s | 2400 s | 58000 s | 990 s | 13000 s | 70000 s | 0 s | 0 s | ||||||||||||||||||||
SoftwareSystems 3184 tasks, max. score: 5608 |
-7 | 565 | 491 | 736 | 124 | 694 | 331 | 878 | 894 | 2001 | 359 | 298 | 282 | ||||||||||||||||||
CPU time | 260 s | 16000 s | 76000 s | 160000 s | 9000 s | 20000 s | 13000 s | 98000 s | 52000 s | 2000 s | 60000 s | 62000 s | 74000 s | ||||||||||||||||||
unreach-call.SoftwareSystems-AWS-C-Common-ReachSafety 175 tasks, max. score: 345 |
-26 | 88 | -2 | 45 | 10 | 208 | 30 | 121 | 273 | 138 | 12 | 0 | 0 | ||||||||||||||||||
CPU time | 48 s | 140 s | 460 s | 3100 s | 270 s | 2200 s | 37 s | 5200 s | 15000 s | 840 s | 1700 s | 0 s | 0 s | ||||||||||||||||||
valid-memsafety.SoftwareSystems-BusyBox-MemSafety 37 tasks, max. score: 67 |
0 | 1 | 0 | 0 | 0 | 0 | 0 | 1 | 5 | 0 | 0 | 0 | |||||||||||||||||||
CPU time | 0 s | 12 s | 0 s | 0 s | 0 s | 0 s | 0 s | 71 s | 65 s | 0 s | 0 s | 0 s | |||||||||||||||||||
no-overflow.SoftwareSystems-BusyBox-NoOverflows 65 tasks, max. score: 96 |
0 | 0 | 0 | 2 | 0 | 0 | 0 | 0 | 2 | 0 | 0 | 2 | 2 | 0 | |||||||||||||||||
CPU time | 0 s | 0 s | 0 s | 480 s | 0 s | 0 s | 0 s | 0 s | 480 s | 0 s | 0 s | 34 s | 57 s | 0 s | |||||||||||||||||
unreach-call.SoftwareSystems-DeviceDriversLinux64-ReachSafety 2503 tasks, max. score: 4667 |
322 | 167 | 3000 | 2744 | 733 | 1932 | 1912 | 2664 | 2356 | 1348 | 2292 | 2033 | 1994 | ||||||||||||||||||
CPU time | 220 s | 16000 s | 75000 s | 160000 s | 8700 s | 17000 s | 13000 s | 92000 s | 37000 s | 530 s | 58000 s | 62000 s | 74000 s | ||||||||||||||||||
unreach-call.SoftwareSystems-DeviceDriversLinux64Large-ReachSafety 10 tasks, max. score: 20 |
0 | 0 | 2 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | ||||||||||||||||||
CPU time | 0 s | 0 s | 540 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | ||||||||||||||||||
valid-memsafety.SoftwareSystems-OpenBSD-MemSafety 4 tasks, max. score: 5 |
0 | 4 | 0 | 0 | 0 | 0 | 0 | 0 | 2 | 0 | 0 | 0 | |||||||||||||||||||
CPU time | 0 s | 4.9 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 17 s | 0 s | 0 s | 0 s | |||||||||||||||||||
valid-memsafety.SoftwareSystems-uthash-MemSafety 138 tasks, max. score: 204 |
0 | 0 | 0 | 96 | 0 | 0 | 96 | 0 | 180 | 0 | 0 | 0 | |||||||||||||||||||
CPU time | 0 s | 0 s | 0 s | 710 s | 0 s | 0 s | 710 s | 0 s | 400 s | 0 s | 0 s | 0 s | |||||||||||||||||||
no-overflow.SoftwareSystems-uthash-NoOverflows 114 tasks, max. score: 228 |
0 | 0 | 0 | 0 | 0 | 0 | 84 | 0 | 0 | 0 | 84 | 0 | 0 | 0 | |||||||||||||||||
CPU time | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 12 s | 0 s | 0 s | 0 s | 40 s | 0 s | 0 s | 0 s | |||||||||||||||||
unreach-call.SoftwareSystems-uthash-ReachSafety 138 tasks, max. score: 276 |
0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 228 | 0 | 0 | 0 | ||||||||||||||||||
CPU time | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 95 s | 0 s | 0 s | 0 s | ||||||||||||||||||
FalsificationOverall 12989 tasks, max. score: 6173 |
1436 | 2609 | 4356 | 306 | 2002 | 4329 | 2947 | 3432 | 1800 | 3336 | |||||||||||||||||||||
CPU time | 28000 s | 43000 s | 250000 s | 110000 s | 100000 s | 170000 s | 45000 s | 110000 s | 33000 s | 76000 s | |||||||||||||||||||||
Overall 15201 tasks, max. score: 23778 |
6219 | 5289 | 12217 | 2083 | 6656 | 12208 | 9268 | 11769 | 4332 | 7676 | |||||||||||||||||||||
CPU time | 95000 s | 93000 s | 690000 s | 160000 s | 220000 s | 450000 s | 74000 s | 360000 s | 170000 s | 270000 s | |||||||||||||||||||||
JavaOverall 473 tasks, max. score: 693 |
298 | 630 | 369 | 603 | 623 | 409 | |||||||||||||||||||||||||
CPU time | 2900 s | 18000 s | 25000 s | 780 s | 3400 s | 2100 s | |||||||||||||||||||||||||
assert_java.ReachSafety-Java 473 tasks, max. score: 693 |
298 | 630 | 369 | 603 | 623 | 409 | |||||||||||||||||||||||||
CPU time | 2900 s | 18000 s | 25000 s | 780 s | 3400 s | 2100 s | |||||||||||||||||||||||||
Participants | Plots | 2LS | BRICK | CBMC | CPA-BAM-BnB | CPALockator | CPAchecker | Dartagnan | DIVINE | ESBMC-incr | ESBMC-kind | Frama-C | Gazer-Theta | Goblint | Korn | Lazy-CSeq | PeSCo | Pinaka | PredatorHP | SMACK | Symbiotic | UAutomizer | UKojak | UTaipan | VeriAbs | COASTAL | Java-Ranger | JayHorn | JBMC | JDart | SPF |
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).