TACAS 2016 | |
5th Competition on Software Verification (SV-COMP) |
This web page presents the results of the 2016 5th International Competition on Software Verification (SV-COMP'16).
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 manupulating 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.
Arrays 1. ESBMC 2. SMACK+Corral 3. Symbiotic |
BitVectors 1. CPA-Seq 2. ESBMC 3. CPA-kInd |
Heap 1. PredatorHP 2. CPA-Seq 3. Cascade |
Floats 1. 2LS 2. Ceagle 3. CBMC |
IntegersControlFlow 1. CPA-Seq 2. CPA-kInd 3. SMACK+Corral |
Termination 1. AProVE 2. UAutomizer 3. SeaHorn |
Concurrency 1. MU-CSeq 2. Lazy-CSeq 3. CIVL |
DeviceDriversLinux64 1. CPA-RefSel 2. CPA-Seq 3. BLAST |
FalsificationOverall 1. UAutomizer 2. SMACK+Corral 3. CPA-kInd |
Overall 1. UAutomizer 2. CPA-Seq 3. SMACK+Corral |
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 | BLAST | Cascade | CBMC | Ceagle | Ceagle-Absref | CIVL | CPA-BAM | CPA-kInd | CPA-RefSel | CPA-Seq | DIVINE | ESBMC | ESBMC+DepthK | Forest | Forester | HIPrec | Impara | Lazy-CSeq | LCTD | LPI | Map2Check | MU-CSeq | PAC-MAN | PredatorHP | SeaHorn | Skink | SMACK+Corral | Symbiotic | SymDIVINE | UAutomizer | UKojak | UL-CSeq | VVT |
Representing Jury Member | Peter Schrammel | Jera Hensel | Vadim Mutilin | Wei Wang | Michael Tautschnig | Dexi Wang | Guang Chen | Stephen Siegel | Karlheinz Friedberger | Matthias Dangl | Stefan Löwe | CPAchecker Team | Vladimír Štill | Mikhail Ramalho | Lucas Cordeiro | Pablo Sanchez | Ondřej Lengál | Quang Loc Le | Björn Wachter | Omar Inverso | Keijo Heljanko | George Karpenkov | Herbert Rocha | Gennaro Parlato | Ming-Hsien Tsai | Tomas Vojnar | Jorge Navas | Franck Cassez | Zvonimir Rakamaric | Jan Strejček | Jiří Barnat | Matthias Heizmann | Daniel Dietsch | Bernd Fischer | Alfons Laarman | |
Affiliation | University of Oxford, UK | RWTH Aachen, Germany | ISPRAS, Russia | New York University, USA | Queen Mary University of London, UK | Tsinghua University, China | Tsinghua University, China | University of Delaware, USA | University of Passau, Germany | University of Passau, Germany | University of Passau, Germany | University of Passau, Germany | Masaryk University, Czech Republic | University of Southampton, UK | Federal University of Amazonas, Brazil | University of Cantabria, Spain | BUT, Brno, Czech Republic | National University, Singapore | University of Oxford, UK | Gran Sasso Science Institute, Italy | Aalto University, Finland | VERIMAG, France | Federal University of Roraima, Brazil | University of Southampton, UK | Academia Sinica, Taiwan | BUT, Brno, Czech Republic | NASA Ames Research Center, USA | Macquarie University, Sydney, Australia | University of Utah, USA | Masaryk University, Czech Republic | Masaryk University, Czech Republic | University of Freiburg, Germany | University of Freiburg, Germany | University of Stellenbosch, ZA | TU Vienna, Austria | |
Arrays 183 tasks, max. score: 316 |
62 | -57 | 3 | -61 | 190 | 62 | -970 | -301 | 146 | 101 | 83 | 60 | ||||||||||||||||||||||||
CPU time | 36000 s | 170 s | 540 s | 1500 s | 12000 s | 1200 s | 3600 s | 1100 s | 9000 s | 2200 s | 1500 s | 600 s | ||||||||||||||||||||||||
ArraysReach 118 tasks, max. score: 202 |
-92 | -73 | 4 | -76 | -89 | 127 | 80 | -71 | 106 | -388 | 188 | 130 | 20 | 6 | ||||||||||||||||||||||
CPU time | 18000 s | 170 s | 540 s | 700 s | 1500 s | 5500 s | 1200 s | 3500 s | 43000 s | 1100 s | 9000 s | 2200 s | 940 s | 27 s | ||||||||||||||||||||||
ArraysMemSafety 65 tasks, max. score: 113 |
5 | 95 | 0 | 0 | 0 | 6 | 65 | 0 | -650 | 0 | 0 | 0 | 48 | 39 | ||||||||||||||||||||||
CPU time | 1700 s | 19000 s | 17 s | 6000 s | 33 s | 540 s | 580 s | |||||||||||||||||||||||||||||
BitVectors 60 tasks, max. score: 92 |
46 | 28 | 77 | 87 | 84 | 47 | -592 | -131 | 44 | -2 | 69 | 19 | ||||||||||||||||||||||||
CPU time | 12000 s | 850 s | 2400 s | 3900 s | 2200 s | 1000 s | 360 s | 780 s | 9600 s | 2000 s | 1600 s | 210 s | ||||||||||||||||||||||||
BitVectorsReach 48 tasks, max. score: 84 |
53 | 50 | -62 | 45 | 59 | 57 | 75 | 70 | 75 | -151 | 44 | 16 | -10 | -209 | 71 | -3 | 46 | 19 | ||||||||||||||||||
CPU time | 300 s | 12000 s | .30 s | 850 s | 2400 s | 2200 s | 3900 s | 2200 s | 1000 s | 1300 s | 360 s | 8.9 s | 18000 s | 780 s | 9600 s | 2000 s | 1500 s | 190 s | ||||||||||||||||||
BitVectorsOverflows 12 tasks, max. score: 16 |
6 | 0 | 16 | 0 | 16 | 16 | 0 | -248 | 0 | 0 | 0 | 16 | 3 | |||||||||||||||||||||||
CPU time | 3.4 s | 51 s | 47 s | 2.5 s | .48 s | 110 s | 17 s | |||||||||||||||||||||||||||||
Heap 239 tasks, max. score: 382 |
197 | 8 | -80 | 161 | 234 | 163 | 58 | -1263 | 86 | -121 | 298 | -257 | 155 | 105 | 169 | 31 | ||||||||||||||||||||
CPU time | 9900 s | 35000 s | 340 s | 510 s | 4100 s | 1100 s | 400 s | 620 s | 44 s | 93 s | 1100 s | 17 s | 6400 s | 560 s | 6800 s | 520 s | ||||||||||||||||||||
HeapReach 81 tasks, max. score: 137 |
82 | 130 | -54 | 109 | 97 | 98 | 81 | 39 | -225 | 39 | 0 | 112 | -174 | 105 | 71 | 97 | 24 | |||||||||||||||||||
CPU time | 6900 s | 18000 s | 340 s | 510 s | 1100 s | 2100 s | 790 s | 400 s | 22 s | 2.7 s | 38 s | 17 s | 6400 s | 560 s | 680 s | 230 s | ||||||||||||||||||||
HeapMemSafety 158 tasks, max. score: 238 |
101 | -243 | 0 | 0 | 0 | 118 | 57 | 0 | -1231 | 38 | -160 | 176 | 0 | 0 | 0 | 34 | -6 | |||||||||||||||||||
CPU time | 3000 s | 17000 s | 2000 s | 340 s | 600 s | 42 s | 93 s | 1100 s | 6200 s | 290 s | ||||||||||||||||||||||||||
Floats 81 tasks, max. score: 140 |
136 | 134 | 136 | 124 | 42 | 76 | 35 | 75 | -15 | 7 | 132 | -449 | 0 | 0 | -18 | 2 | 0 | |||||||||||||||||||
CPU time | 3500 s | 18000 s | 3700 s | 2400 s | 5700 s | 4900 s | 1200 s | 2500 s | 4500 s | 4.3 s | 5700 s | 32000 s | 19 s | 17 s | ||||||||||||||||||||||
IntegersControlFlow 2331 tasks, max. score: 3629 |
1196 | -1653 | -1239 | 1822 | 2095 | 1539 | 2652 | 1217 | 1111 | -1524 | 1804 | 1572 | 113 | 2013 | 633 | 1865 | 1096 | 421 | ||||||||||||||||||
CPU time | 70000 s | 28000 s | 750000 s | 38000 s | 130000 s | 120000 s | 130000 s | 62000 s | 5700 s | 23000 s | 83000 s | 40000 s | 370 s | 350000 s | 32000 s | 76000 s | 8300 s | 5600 s | ||||||||||||||||||
ControlFlow 48 tasks, max. score: 78 |
62 | 51 | 77 | 38 | 76 | 68 | 78 | 53 | 73 | -248 | 48 | 61 | 72 | 0 | 61 | 12 | 77 | 38 | 40 | |||||||||||||||||
CPU time | 680 s | 2900 s | 17000 s | 200 s | 1100 s | 5500 s | 2400 s | 6200 s | 480 s | 330 s | 1300 s | 700 s | 630 s | 8400 s | 3000 s | 1800 s | 510 s | 3000 s | ||||||||||||||||||
Simple 46 tasks, max. score: 68 |
-20 | 12 | 12 | 54 | 38 | 17 | 48 | 32 | 0 | -30 | 14 | 58 | 0 | 44 | 0 | 0 | 0 | 0 | ||||||||||||||||||
CPU time | 3100 s | 1200 s | 18000 s | 2500 s | 1900 s | 2900 s | 5800 s | 6200 s | 1.8 s | 970 s | 970 s | 15000 s | ||||||||||||||||||||||||
ECA 1140 tasks, max. score: 1874 |
652 | -40 | -7140 | 296 | 867 | 788 | 1066 | 306 | 33 | 0 | 823 | -789 | 0 | 228 | 2 | 745 | 3 | 88 | ||||||||||||||||||
CPU time | 47000 s | 5000 s | 620000 s | 5800 s | 51000 s | 97000 s | 83000 s | 44000 s | 420 s | 39000 s | 23000 s | 91000 s | 560 s | 46000 s | 77 s | 1500 s | ||||||||||||||||||||
Loops 141 tasks, max. score: 234 |
136 | -256 | -69 | 88 | 131 | 76 | 130 | 15 | 26 | -313 | 114 | 174 | 48 | 48 | 110 | 84 | 131 | 135 | ||||||||||||||||||
CPU time | 320 s | 770 s | 14000 s | 1100 s | 1000 s | 1100 s | 3600 s | 420 s | 2300 s | 500 s | 2500 s | 2300 s | 3100 s | 370 s | 41000 s | 2200 s | 3900 s | 1900 s | ||||||||||||||||||
Recursive 98 tasks, max. score: 151 |
0 | -256 | 12 | -218 | 121 | 10 | 10 | 118 | 32 | 15 | -388 | 111 | -673 | 8 | 106 | 131 | 0 | 97 | 89 | 110 | 69 | |||||||||||||||
CPU time | 12 s | 16000 s | .40 s | 610 s | 26 s | 27 s | 590 s | 1100 s | 24 s | 1500 s | 210 s | 9.6 s | 21 s | 29000 s | 350 s | 15000 s | 1800 s | 2400 s | 800 s | |||||||||||||||||
ProductLines 597 tasks, max. score: 929 |
633 | 613 | 760 | 730 | 866 | 929 | 929 | 579 | 760 | 597 | 754 | 858 | 0 | 875 | 253 | 646 | 479 | |||||||||||||||||||
CPU time | 13000 s | 16000 s | 8900 s | 25000 s | 54000 s | 11000 s | 9000 s | 1300 s | 1900 s | 18000 s | 32000 s | 3400 s | 160000 s | 21000 s | 16000 s | 4800 s | ||||||||||||||||||||
Sequentialized 261 tasks, max. score: 364 |
36 | -744 | -60 | 43 | 167 | -14 | 177 | 48 | 46 | 35 | 141 | -121 | 0 | 100 | -73 | 55 | 9 | |||||||||||||||||||
CPU time | 6600 s | 2000 s | 51000 s | 2800 s | 17000 s | 1700 s | 23000 s | 2800 s | 580 s | 330 s | 9000 s | 8800 s | 24000 s | 2700 s | 4900 s | 250 s | ||||||||||||||||||||
Termination 631 tasks, max. score: 1129 |
909 | 0 | 0 | 0 | 0 | 0 | 0 | 504 | 0 | 0 | 895 | |||||||||||||||||||||||||
CPU time | 17000 s | 3500 s | 12000 s | |||||||||||||||||||||||||||||||||
Concurrency 1016 tasks, max. score: 1240 |
882 | 1240 | 0 | 0 | 0 | 282 | 951 | 742 | 877 | -20613 | 42 | 1240 | 1240 | -24659 | 999 | 0 | -135 | 856 | 1029 | |||||||||||||||||
CPU time | 84000 s | 28000 s | 11000 s | 84000 s | 70000 s | 19000 s | 2800 s | 20000 s | 9600 s | 3400 s | 55 s | 85000 s | 1800 s | 110000 s | 71000 s | |||||||||||||||||||||
DeviceDriversLinux64 2120 tasks, max. score: 3977 |
2704 | 1972 | 2550 | 2350 | 3177 | 2801 | 1688 | 2009 | 2107 | 1694 | 2206 | 980 | 2686 | 937 | ||||||||||||||||||||||
CPU time | 21000 s | 800000 s | 33000 s | 45000 s | 87000 s | 84000 s | 35000 s | 49000 s | 51000 s | 21000 s | 100000 s | 550 s | 62000 s | 66000 s | ||||||||||||||||||||||
FalsificationOverall 6030 tasks, max. score: 2371 |
-2438 | 391 | -1218 | 707 | 36 | 496 | 248 | 495 | -4333 | 800 | -370 | 823 | 339 | |||||||||||||||||||||||
CPU time | 31000 s | 52000 s | 29000 s | 51000 s | 88000 s | 44000 s | 94000 s | 18000 s | 7500 s | 61000 s | 27000 s | 25000 s | 4000 s | |||||||||||||||||||||||
Overall 6661 tasks, max. score: 10855 |
-38205 | 3386 | 1939 | 4094 | 2157 | 4794 | 4145 | 3110 | -22393 | 4223 | 1223 | 4843 | 1407 | |||||||||||||||||||||||
CPU time | 85000 s | 1700000 s | 78000 s | 180000 s | 210000 s | 230000 s | 190000 s | 77000 s | 67000 s | 560000 s | 37000 s | 160000 s | 75000 s | |||||||||||||||||||||||
Verifiers | Plots | 2LS | AProVE | BLAST | Cascade | CBMC | Ceagle | Ceagle-Absref | CIVL | CPA-BAM | CPA-kInd | CPA-RefSel | CPA-Seq | DIVINE | ESBMC | ESBMC+DepthK | Forest | Forester | HIPrec | Impara | Lazy-CSeq | LCTD | LPI | Map2Check | MU-CSeq | PAC-MAN | PredatorHP | SeaHorn | Skink | SMACK+Corral | Symbiotic | SymDIVINE | UAutomizer | UKojak | UL-CSeq | VVT |
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.