TACAS 2019 | |
8th Competition on Software Verification (SV-COMP) |
This web page presents the results of the 2019 8th International Competition on Software Verification (SV-COMP '19).
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:
What you can learn from a score-based quantile plot and how to interpret it, is described in the competition report on pages 12 and 13.
ReachSafety 1. VeriAbs 2. CPA-Seq 3. PeSCo |
MemSafety 1. Symbiotic 2. PredatorHP 3. CPA-Seq |
ConcurrencySafety 1. Yogar-CBMC 2. Lazy-CSeq 3. CPA-Seq |
NoOverflows 1. UAutomizer 2. UTaipan 3. CPA-Seq |
Termination 1. UAutomizer 2. AProVE 3. CPA-Seq |
SoftwareSystems 1. CPA-BAM-BnB 2. CPA-Seq 3. VeriAbs |
C-FalsificationOverall 1. CPA-Seq 2. PeSCo 3. ESBMC-kind |
C-Overall 1. CPA-Seq 2. PeSCo 3. UAutomizer |
|
Java-Overall 1. JBMC 2. SPF 3. JPF |
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.
Verifiers | Plots | 2LS | AProVE | CBMC | CBMC-Path | CPA-BAM-BnB | CPA-Lockator | CPA-Seq | DepthK | DIVINE-explicit | DIVINE-SMT | ESBMC-kind | JayHorn | JBMC | JPF | Lazy-CSeq | Map2Check | PeSCo | Pinaka | PredatorHP | Skink | SMACK | SPF | Symbiotic | UAutomizer | UKojak | UTaipan | VeriAbs | VeriFuzz | VIAP | Yogar-CBMC | Yogar-CBMC-Parallel |
Representing Jury Member | Peter Schrammel | Jera Hensel | Michael Tautschnig | Kareem Khazem | Vadim Mutilin | Pavel Andrianov | Marie-Christine Jakobs | Omar Alhawi | Vladimír Štill | Henrich Lauko | Mikhail R. Gadelha | Philipp Ruemmer | Lucas Cordeiro | Cyrille Artho | Omar Inverso | Herbert Rocha | Cedric Richter | Eti Chaudhary | Veronika Šoková | Franck Cassez | Zvonimir Rakamaric | Willem Visser | Marek Chalupa | Matthias Heizmann | Alexander Nutz | Daniel Dietsch | Priyanka Darke | Raveendra Kumar Medicherla | Pritom Rajkhowa | Liangze Yin | Haining Feng | |
Affiliation | University of Sussex, UK | RWTH Aachen, Germany | Amazon Web Services, UK | University College London, UK | ISP RAS, Russia | ISP RAS, Russia | LMU Munich, Germany | University of Manchester, UK | Masaryk University, Czechia | Masaryk University, Czechia | University of Southampton, UK | Uppsala University, Sweden | University of Manchester, UK | KTH, Denmark | Gran Sasso Science Institute, Italy | Federal University of Roraima, Brazil | University of Paderborn, Germany | IIT Hyderabad, India | BUT, Brno, Czechia | Macquarie University, Australia | University of Utah, USA | Stellenbosch University, South Africa | Masaryk University, Czechia | University of Freiburg, Germany | University of Freiburg, Germany | University of Freiburg, Germany | Tata Consultancy Services, India | TCS Research, India | Hong Kong University of Science and Technology, China | National University of Defense Technology, China | National University of Defense Technology, China | |
ReachSafety 3831 tasks, max. score: 6296 |
2397 | 2781 | 1657 | 4299 | 986 | 1413 | 1778 | 3404 | 4239 | *) | 3143 | 3264 | 2195 | 3012 | 4638 | 1132 | ||||||||||||||||
CPU time | 60000 s | 33000 s | 20000 s | 220000 s | 49000 s | 6500 s | 43000 s | 90000 s | 210000 s | 25000 s | 150000 s | 120000 s | 180000 s | 400000 s | 85000 s | |||||||||||||||||
ReachSafety-Arrays 231 tasks, max. score: 418 |
-29 | 32 | 19 | 11 | -11 | 3 | 52 | 31 | 7 | 25 | 129 | 49 | 210 | 18 | 18 | 18 | 365 | 33 | 378 | |||||||||||||
CPU time | 37 s | 640 s | 620 s | 720 s | 72 s | 420 s | 1500 s | 960 s | 790 s | 910 s | 8100 s | 380 s | 1300 s | 150 s | 1300 s | 170 s | 4300 s | 340 s | 9000 s | |||||||||||||
ReachSafety-BitVectors 50 tasks, max. score: 86 |
53 | 50 | 22 | 75 | 11 | 17 | 26 | 57 | 12 | 72 | 40 | 37 | 50 | 62 | 37 | 62 | 57 | 13 | ||||||||||||||
CPU time | 110 s | 330 s | 22 s | 1300 s | 40 s | 89 s | 280 s | 310 s | 150 s | 1100 s | 91 s | 230 s | 100 s | 2800 s | 1200 s | 3100 s | 2400 s | 370 s | ||||||||||||||
ReachSafety-ControlFlow 94 tasks, max. score: 146 |
59 | 62 | 12 | 126 | 36 | 0 | 2 | 83 | -59 | 129 | 26 | 24 | 60 | 84 | 43 | 49 | 67 | 20 | ||||||||||||||
CPU time | 87 s | 340 s | 210 s | 4100 s | 840 s | 0 s | 1000 s | 480 s | 7.4 s | 3300 s | 48 s | 58 s | 18 s | 3500 s | 4300 s | 3500 s | 5300 s | 640 s | ||||||||||||||
ReachSafety-ECA 1256 tasks, max. score: 2041 |
604 | 130 | 4 | 1099 | 144 | 0 | 2 | 1113 | 978 | 261 | 82 | 835 | 349 | 773 | 1515 | 430 | ||||||||||||||||
CPU time | 48000 s | 21000 s | 110 s | 110000 s | 41000 s | 0 s | 1600 s | 78000 s | 99000 s | 19000 s | 2800 s | 85000 s | 56000 s | 110000 s | 120000 s | 55000 s | ||||||||||||||||
ReachSafety-Floats 469 tasks, max. score: 893 |
721 | 800 | 792 | 761 | 36 | 442 | 426 | 790 | 737 | 807 | 531 | 688 | 459 | 635 | 438 | 635 | 823 | 43 | ||||||||||||||
CPU time | 2700 s | 6100 s | 7900 s | 11000 s | 980 s | 2300 s | 2200 s | 7600 s | 20000 s | 1500 s | 3800 s | 25000 s | 55 s | 30000 s | 31000 s | 31000 s | 32000 s | 910 s | ||||||||||||||
ReachSafety-Heap 241 tasks, max. score: 407 |
141 | 288 | 233 | 293 | 188 | 221 | 252 | 300 | -7 | 282 | 236 | 262 | 138 | 298 | 204 | 222 | 165 | 305 | 66 | |||||||||||||
CPU time | 150 s | 190 s | 8200 s | 3100 s | 960 s | 1400 s | 1600 s | 270 s | 1400 s | 4800 s | 79 s | 67 s | 580 s | 43 s | 4000 s | 3400 s | 4300 s | 11000 s | 500 s | |||||||||||||
ReachSafety-Loops 208 tasks, max. score: 357 |
140 | 136 | 65 | 226 | 38 | 85 | 123 | 130 | -79 | 224 | 95 | 190 | 180 | 212 | 224 | 222 | 275 | 48 | 178 | |||||||||||||
CPU time | 500 s | 1200 s | 150 s | 7000 s | 86 s | 1100 s | 2200 s | 1700 s | 1300 s | 4800 s | 570 s | 1600 s | 180 s | 3700 s | 4700 s | 3700 s | 12000 s | 200 s | 3500 s | |||||||||||||
ReachSafety-ProductLines 597 tasks, max. score: 929 |
732 | 284 | 134 | 918 | 265 | 134 | 248 | 787 | 909 | 314 | 898 | 453 | 630 | 308 | 612 | 904 | 265 | |||||||||||||||
CPU time | 6900 s | 500 s | 2100 s | 7400 s | 1200 s | 690 s | 16000 s | 600 s | 39000 s | 1000 s | 150000 s | 280 s | 9200 s | 5000 s | 14000 s | 95000 s | 2700 s | |||||||||||||||
ReachSafety-Recursive 96 tasks, max. score: 148 |
0 | 99 | 45 | 111 | 36 | 81 | 99 | 99 | 37 | 112 | 99 | 53 | 102 | 120 | 62 | 113 | 107 | 43 | 124 | |||||||||||||
CPU time | 0 s | 310 s | 1100 s | 1200 s | 57 s | 450 s | 1300 s | 370 s | 48 s | 2100 s | 530 s | 420 s | 17 s | 3000 s | 1100 s | 5200 s | 7800 s | 1500 s | 710 s | |||||||||||||
ReachSafety-Sequentialized 589 tasks, max. score: 778 |
113 | 175 | 7 | 494 | 27 | 0 | -70 | -36 | 505 | 401 | 406 | 70 | 48 | 59 | 292 | 300 | ||||||||||||||||
CPU time | 2100 s | 2500 s | 19 s | 69000 s | 4200 s | 0 s | 15000 s | 280 s | 34000 s | 21000 s | 21000 s | 12000 s | 9800 s | 9900 s | 110000 s | 23000 s | ||||||||||||||||
MemSafety 434 tasks, max. score: 649 |
129 | 60 | -59 | 349 | -113 | 25 | -158 | -208 | 38 | 416 | *) | 426 | -163 | -211 | -91 | |||||||||||||||||
CPU time | 470 s | 1600 s | 7700 s | 2000 s | 2800 s | 1500 s | 1600 s | 1800 s | 16000 s | 2200 s | 110 s | 8300 s | 13000 s | 8300 s | ||||||||||||||||||
MemSafety-Arrays 71 tasks, max. score: 120 |
0 | 4 | 12 | 4 | 20 | 1 | 6 | 18 | 91 | -44 | 14 | 14 | 103 | 69 | 101 | |||||||||||||||||
CPU time | 0 s | 13 s | 1.1 s | 11 s | 5.0 s | 8.3 s | 51 s | 2.5 s | 4300 s | 11 s | 2.6 s | 5.6 s | 1300 s | 2100 s | 1600 s | |||||||||||||||||
MemSafety-Heap 180 tasks, max. score: 270 |
56 | 116 | 94 | 183 | -95 | 0 | -125 | 120 | 140 | 183 | 204 | 194 | 73 | 84 | 73 | |||||||||||||||||
CPU time | 280 s | 1200 s | 71 s | 760 s | 1900 s | 690 s | 720 s | 1300 s | 7500 s | 770 s | 960 s | 36 s | 3400 s | 7400 s | 5200 s | |||||||||||||||||
MemSafety-LinkedLists 103 tasks, max. score: 178 |
-20 | 55 | 54 | 114 | 50 | 88 | 41 | 107 | 112 | 114 | 148 | 121 | 126 | 21 | 11 | 6 | ||||||||||||||||
CPU time | 150 s | 360 s | 7500 s | 600 s | 800 s | 700 s | 720 s | 460 s | 3300 s | 580 s | 33 s | 11000 s | 33 s | 3100 s | 2500 s | 940 s | ||||||||||||||||
MemSafety-Other 48 tasks, max. score: 75 |
49 | -26 | -91 | 42 | -26 | -28 | -77 | -209 | -130 | 42 | 58 | 52 | 69 | 3 | 1 | 3 | ||||||||||||||||
CPU time | 7.9 s | 24 s | 110 s | 470 s | 2.9 s | 130 s | 120 s | 25 s | 700 s | 460 s | 1200 s | 1900 s | 25 s | 550 s | 980 s | 550 s | ||||||||||||||||
MemSafety-MemCleanup 32 tasks, max. score: 32 |
11 | 0 | 0 | 31 | -32 | 0 | 0 | 0 | 0 | 0 | 26 | 28 | 31 | -128 | -128 | -96 | ||||||||||||||||
CPU time | 37 s | 0 s | 0 s | 130 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 7.9 s | 110 s | 7.9 s | 0 s | 0 s | 0 s | ||||||||||||||||
ConcurrencySafety 1082 tasks, max. score: 1344 |
0 | 613 | -150 | -441 | 996 | 420 | 493 | 339 | 404 | 1245 | *) | 0 | 270 | 0 | 271 | 1277 | ||||||||||||||||
CPU time | 0 s | 1700 s | 1100 s | 1200 s | 48000 s | 4500 s | 7800 s | 23000 s | 3300 s | 11000 s | 0 s | 2500 s | 0 s | 3400 s | 1100 s | |||||||||||||||||
ConcurrencySafety-Main 1082 tasks, max. score: 1344 |
0 | 613 | -150 | -441 | 996 | 420 | 493 | 339 | 404 | 1245 | 937 | 0 | 270 | 0 | 271 | 1277 | 1273 | |||||||||||||||
CPU time | 0 s | 1700 s | 1100 s | 1200 s | 48000 s | 4500 s | 7800 s | 23000 s | 3300 s | 11000 s | 55000 s | 0 s | 2500 s | 0 s | 3400 s | 1100 s | 3200 s | |||||||||||||||
NoOverflows 359 tasks, max. score: 574 |
280 | 227 | 192 | 431 | 39 | 0 | 0 | 224 | 8 | 218 | *) | 331 | 449 | 396 | 438 | 123 | ||||||||||||||||
CPU time | 96 s | 56 s | 140 s | 2100 s | 3.4 s | 0 s | 0 s | 68 s | 2300 s | 160 s | 260 s | 3400 s | 3400 s | 3400 s | 5300 s | |||||||||||||||||
NoOverflows-BitVectors 280 tasks, max. score: 402 |
273 | 191 | 161 | 311 | 0 | 0 | 0 | 187 | 12 | 311 | 177 | 204 | 350 | 309 | 346 | 131 | ||||||||||||||||
CPU time | 92 s | 51 s | 130 s | 1200 s | 0 s | 0 s | 0 s | 42 s | 470 s | 1200 s | 64 s | 52 s | 2800 s | 2900 s | 2800 s | 5300 s | ||||||||||||||||
NoOverflows-Other 79 tasks, max. score: 139 |
46 | 46 | 39 | 102 | 17 | 0 | 0 | 46 | 0 | 102 | 46 | 88 | 99 | 87 | 95 | 17 | ||||||||||||||||
CPU time | 4.0 s | 4.8 s | 12 s | 870 s | 3.4 s | 0 s | 0 s | 26 s | 1800 s | 860 s | 93 s | 210 s | 610 s | 440 s | 590 s | 68 s | ||||||||||||||||
Termination 2007 tasks, max. score: 3529 |
1279 | 2476 | 827 | 535 | 1785 | 37 | 0 | 0 | 826 | 561 | *) | 1153 | 3001 | 0 | 0 | |||||||||||||||||
CPU time | 7300 s | 120000 s | 4400 s | 2600 s | 56000 s | 180 s | 0 s | 0 s | 2800 s | 2700 s | 8800 s | 46000 s | 0 s | 0 s | ||||||||||||||||||
Termination-MainControlFlow 249 tasks, max. score: 443 |
275 | 397 | 60 | 48 | 320 | 0 | 0 | 0 | 60 | 290 | 52 | 154 | 401 | 0 | 0 | |||||||||||||||||
CPU time | 51 s | 2800 s | 20 s | 12 s | 2800 s | 0 s | 0 s | 0 s | 210 s | 2800 s | 19 s | 710 s | 3100 s | 0 s | 0 s | |||||||||||||||||
Termination-MainHeap 259 tasks, max. score: 502 |
-26 | 340 | 24 | 22 | 65 | 0 | 0 | 0 | 24 | 59 | 22 | 72 | 405 | 0 | 0 | |||||||||||||||||
CPU time | 4.2 s | 6100 s | 16 s | 13 s | 4700 s | 110 s | 0 s | 0 s | 510 s | 4400 s | 120 s | 10 s | 4900 s | 0 s | 0 s | |||||||||||||||||
Termination-Other 1499 tasks, max. score: 2335 |
1361 | 1189 | 1352 | 782 | 1696 | 84 | 0 | 0 | 1350 | 1582 | 816 | 1240 | 1967 | 0 | 0 | |||||||||||||||||
CPU time | 7200 s | 110000 s | 4400 s | 2600 s | 48000 s | 73 s | 0 s | 0 s | 2000 s | 41000 s | 2600 s | 8100 s | 38000 s | 0 s | 0 s | |||||||||||||||||
SoftwareSystems 2809 tasks, max. score: 4955 |
119 | 0 | -151 | 1185 | 1073 | -1182 | 2 | 0 | 714 | *) | 555 | 1020 | 818 | 962 | 1061 | |||||||||||||||||
CPU time | 180 s | 600 s | 360 s | 33000 s | 99000 s | 0 s | 17 s | 0 s | 20000 s | 250 s | 92000 s | 63000 s | 61000 s | 87000 s | ||||||||||||||||||
Systems_BusyBox_MemSafety 40 tasks, max. score: 76 |
0 | 0 | 0 | 0 | 0 | -32 | 0 | 0 | 1 | 0 | 1 | 0 | 0 | 0 | 0 | |||||||||||||||||
CPU time | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 0 s | 540 s | 0 s | .65 s | 0 s | 0 s | 0 s | 0 s | |||||||||||||||||
Systems_BusyBox_NoOverflows 71 tasks, max. score: 108 |
0 | 0 | 0 | 0 | 0 | -32 | 0 | 0 | 0 | 0 | 0 | 2 | 2 | 2 | 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 | 18 s | 33 s | 19 s | 0 s | |||||||||||||||||
Systems_DeviceDriversLinux64_ReachSafety 2698 tasks, max. score: 5046 |
343 | 0 | -434 | 3415 | 3093 | -32 | 6 | 0 | 1990 | 2933 | 1532 | 2862 | 2280 | 2695 | 3056 | |||||||||||||||||
CPU time | 180 s | 600 s | 360 s | 33000 s | 99000 s | 0 s | 17 s | 0 s | 20000 s | 100000 s | 250 s | 92000 s | 63000 s | 61000 s | 87000 s | |||||||||||||||||
C-FalsificationOverall 8515 tasks, max. score: 3843 |
733 | 1432 | 81 | 2823 | 129 | 200 | -339 | 1916 | 2313 | *) | 1828 | 1050 | 1060 | 1024 | ||||||||||||||||||
CPU time | 22000 s | 27000 s | 5200 s | 140000 s | 51000 s | 4800 s | 47000 s | 53000 s | 190000 s | 23000 s | 59000 s | 35000 s | 56000 s | |||||||||||||||||||
C-Overall 10522 tasks, max. score: 16663 |
4174 | 4341 | 1587 | 9329 | 159 | 1547 | 726 | 3636 | 8466 | *) | 6129 | 6727 | 2595 | 4188 | ||||||||||||||||||
CPU time | 68000 s | 41000 s | 32000 s | 420000 s | 57000 s | 16000 s | 67000 s | 120000 s | 420000 s | 35000 s | 310000 s | 200000 s | 260000 s | |||||||||||||||||||
Java-Overall 368 tasks, max. score: 532 |
247 | 470 | 290 | 365 | ||||||||||||||||||||||||||||
CPU time | 2100 s | 9700 s | 550 s | 970 s | ||||||||||||||||||||||||||||
ReachSafety-Java 368 tasks, max. score: 532 |
247 | 470 | 290 | 365 | ||||||||||||||||||||||||||||
CPU time | 2100 s | 9700 s | 550 s | 970 s | ||||||||||||||||||||||||||||
Verifiers | Plots | 2LS | AProVE | CBMC | CBMC-Path | CPA-BAM-BnB | CPA-Lockator | CPA-Seq | DepthK | DIVINE-explicit | DIVINE-SMT | ESBMC-kind | JayHorn | JBMC | JPF | Lazy-CSeq | Map2Check | PeSCo | Pinaka | PredatorHP | Skink | SMACK | SPF | Symbiotic | UAutomizer | UKojak | UTaipan | VeriAbs | VeriFuzz | VIAP | Yogar-CBMC | Yogar-CBMC-Parallel |
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.
*) The verifier SMACK has been disqualified from several categories because the verifier uses file names of verification tasks to set parameters of the verification engine in an internal wrapper script, more precisely: (a) loop bound of bounded model checking is set depending on file names, (b) returned result is set without performing actual verification work, (c) context-switch bound and mode is set depending on file names, (d) internal time limit is set depending on file names, and (e) missing support for strcpy is detected based on file names for some verification tasks.