TACAS Logo TACAS 2016
5th Competition on Software Verification (SV-COMP)

Results of the Competition

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:


Ranking by Category (with Score-Based Quantile Plots)

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
Quantile-Plot
BitVectors
1. CPA-Seq
2. ESBMC
3. CPA-kInd
Quantile-Plot
Heap
1. PredatorHP
2. CPA-Seq
3. Cascade
Quantile-Plot
Floats
1. 2LS
2. Ceagle
3. CBMC
Quantile-Plot
IntegersControlFlow
1. CPA-Seq
2. CPA-kInd
3. SMACK+Corral
Quantile-Plot
Termination
1. AProVE
2. UAutomizer
3. SeaHorn
Quantile-Plot
Concurrency
1. MU-CSeq
2. Lazy-CSeq
3. CIVL
Quantile-Plot
DeviceDriversLinux64
1. CPA-RefSel
2. CPA-Seq
3. BLAST
Quantile-Plot
FalsificationOverall
1. UAutomizer
2. SMACK+Corral
3. CPA-kInd
Quantile-Plot
Overall
1. UAutomizer
2. CPA-Seq
3. SMACK+Corral
Quantile-Plot

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.

VerifiersPlots2LSAProVEBLASTCascadeCBMCCeagleCeagle-AbsrefCIVLCPA-BAMCPA-kIndCPA-RefSelCPA-SeqDIVINEESBMCESBMC+DepthKForestForesterHIPrecImparaLazy-CSeqLCTDLPIMap2CheckMU-CSeqPAC-MANPredatorHPSeaHornSkinkSMACK+CorralSymbioticSymDIVINEUAutomizerUKojakUL-CSeqVVT
Representing Jury MemberPeter SchrammelJera HenselVadim MutilinWei WangMichael TautschnigDexi WangGuang ChenStephen SiegelKarlheinz FriedbergerMatthias DanglStefan LöweCPAchecker TeamVladimír ŠtillMikhail RamalhoLucas CordeiroPablo SanchezOndřej LengálQuang Loc LeBjörn WachterOmar InversoKeijo HeljankoGeorge KarpenkovHerbert RochaGennaro ParlatoMing-Hsien TsaiTomas VojnarJorge NavasFranck CassezZvonimir RakamaricJan StrejčekJiří BarnatMatthias HeizmannDaniel DietschBernd FischerAlfons Laarman
AffiliationUniversity of Oxford, UKRWTH Aachen, GermanyISPRAS, RussiaNew York University, USAQueen Mary University of London, UKTsinghua University, ChinaTsinghua University, ChinaUniversity of Delaware, USAUniversity of Passau, GermanyUniversity of Passau, GermanyUniversity of Passau, GermanyUniversity of Passau, GermanyMasaryk University, Czech RepublicUniversity of Southampton, UKFederal University of Amazonas, BrazilUniversity of Cantabria, SpainBUT, Brno, Czech RepublicNational University, SingaporeUniversity of Oxford, UKGran Sasso Science Institute, ItalyAalto University, FinlandVERIMAG, FranceFederal University of Roraima, BrazilUniversity of Southampton, UKAcademia Sinica, TaiwanBUT, Brno, Czech RepublicNASA Ames Research Center, USAMacquarie University, Sydney, AustraliaUniversity of Utah, USAMasaryk University, Czech RepublicMasaryk University, Czech RepublicUniversity of Freiburg, GermanyUniversity of Freiburg, GermanyUniversity of Stellenbosch, ZATU Vienna, Austria
Arrays
183 tasks, max. score: 316
Quantile-Plot 62-573-6119062-970-3011461018360
CPU time36000 s170 s540 s1500 s12000 s1200 s3600 s1100 s9000 s2200 s1500 s600 s
ArraysReach
118 tasks, max. score: 202
Quantile-Plot -92-734-76-8912780-71106-388188130206
CPU time18000 s170 s540 s700 s1500 s5500 s1200 s3500 s43000 s1100 s9000 s2200 s940 s27 s
ArraysMemSafety
65 tasks, max. score: 113
Quantile-Plot 5950006650-6500004839
CPU time1700 s19000 s17 s6000 s33 s540 s580 s
BitVectors
60 tasks, max. score: 92
Quantile-Plot 462877878447-592-13144-26919
CPU time12000 s850 s2400 s3900 s2200 s1000 s360 s780 s9600 s2000 s1600 s210 s
BitVectorsReach
48 tasks, max. score: 84
Quantile-Plot 5350-62455957757075-1514416-10-20971-34619
CPU time300 s12000 s.30 s850 s2400 s2200 s3900 s2200 s1000 s1300 s360 s8.9 s18000 s780 s9600 s2000 s1500 s190 s
BitVectorsOverflows
12 tasks, max. score: 16
Quantile-Plot 6016016160-248000163
CPU time3.4 s51 s47 s2.5 s.48 s110 s17 s
Heap
239 tasks, max. score: 382
Quantile-Plot 1978-8016123416358-126386-121298-25715510516931
CPU time9900 s35000 s340 s510 s4100 s1100 s400 s620 s44 s93 s1100 s17 s6400 s560 s6800 s520 s
HeapReach
81 tasks, max. score: 137
Quantile-Plot 82130-5410997988139-225390112-174105719724
CPU time6900 s18000 s340 s510 s1100 s2100 s790 s400 s22 s2.7 s38 s17 s6400 s560 s680 s230 s
HeapMemSafety
158 tasks, max. score: 238
Quantile-Plot 101-243000118570-123138-16017600034-6
CPU time3000 s17000 s2000 s340 s600 s42 s93 s1100 s6200 s290 s
Floats
81 tasks, max. score: 140
Quantile-Plot 13613413612442763575-157132-44900-1820
CPU time3500 s18000 s3700 s2400 s5700 s4900 s1200 s2500 s4500 s4.3 s5700 s32000 s19 s17 s
IntegersControlFlow
2331 tasks, max. score: 3629
Quantile-Plot 1196-1653-1239182220951539265212171111-152418041572113201363318651096421
CPU time70000 s28000 s750000 s38000 s130000 s120000 s130000 s62000 s5700 s23000 s83000 s40000 s370 s350000 s32000 s76000 s8300 s5600 s
ControlFlow
48 tasks, max. score: 78
Quantile-Plot 625177387668785373-24848617206112773840
CPU time680 s2900 s17000 s200 s1100 s5500 s2400 s6200 s480 s330 s1300 s700 s630 s8400 s3000 s1800 s510 s3000 s
Simple
46 tasks, max. score: 68
Quantile-Plot -20121254381748320-3014580440000
CPU time3100 s1200 s18000 s2500 s1900 s2900 s5800 s6200 s1.8 s970 s970 s15000 s
ECA
1140 tasks, max. score: 1874
Quantile-Plot 652-40-71402968677881066306330823-78902282745388
CPU time47000 s5000 s620000 s5800 s51000 s97000 s83000 s44000 s420 s39000 s23000 s91000 s560 s46000 s77 s1500 s
Loops
141 tasks, max. score: 234
Quantile-Plot 136-256-6988131761301526-313114174484811084131135
CPU time320 s770 s14000 s1100 s1000 s1100 s3600 s420 s2300 s500 s2500 s2300 s3100 s370 s41000 s2200 s3900 s1900 s
Recursive
98 tasks, max. score: 151
Quantile-Plot 0-25612-21812110101183215-388111-67381061310978911069
CPU time12 s16000 s.40 s610 s26 s27 s590 s1100 s24 s1500 s210 s9.6 s21 s29000 s350 s15000 s1800 s2400 s800 s
ProductLines
597 tasks, max. score: 929
Quantile-Plot 6336137607308669299295797605977548580875253646479
CPU time13000 s16000 s8900 s25000 s54000 s11000 s9000 s1300 s1900 s18000 s32000 s3400 s160000 s21000 s16000 s4800 s
Sequentialized
261 tasks, max. score: 364
Quantile-Plot 36-744-6043167-14177484635141-1210100-73559
CPU time6600 s2000 s51000 s2800 s17000 s1700 s23000 s2800 s580 s330 s9000 s8800 s24000 s2700 s4900 s250 s
Termination
631 tasks, max. score: 1129
Quantile-Plot 90900000050400895
CPU time17000 s3500 s12000 s
Concurrency
1016 tasks, max. score: 1240
Quantile-Plot 8821240000282951742877-206134212401240-246599990-1358561029
CPU time84000 s28000 s11000 s84000 s70000 s19000 s2800 s20000 s9600 s3400 s55 s85000 s1800 s110000 s71000 s
DeviceDriversLinux64
2120 tasks, max. score: 3977
Quantile-Plot 270419722550235031772801168820092107169422069802686937
CPU time21000 s800000 s33000 s45000 s87000 s84000 s35000 s49000 s51000 s21000 s100000 s550 s62000 s66000 s
FalsificationOverall
6030 tasks, max. score: 2371
Quantile-Plot -2438391-121870736496248495-4333800-370823339
CPU time31000 s52000 s29000 s51000 s88000 s44000 s94000 s18000 s7500 s61000 s27000 s25000 s4000 s
Overall
6661 tasks, max. score: 10855
Quantile-Plot -382053386193940942157479441453110-223934223122348431407
CPU time85000 s1700000 s78000 s180000 s210000 s230000 s190000 s77000 s67000 s560000 s37000 s160000 s75000 s
VerifiersPlots2LSAProVEBLASTCascadeCBMCCeagleCeagle-AbsrefCIVLCPA-BAMCPA-kIndCPA-RefSelCPA-SeqDIVINEESBMCESBMC+DepthKForestForesterHIPrecImparaLazy-CSeqLCTDLPIMap2CheckMU-CSeqPAC-MANPredatorHPSeaHornSkinkSMACK+CorralSymbioticSymDIVINEUAutomizerUKojakUL-CSeqVVT

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.