TACAS Logo TACAS 2017
6th Competition on Software Verification (SV-COMP)

Results of the Competition

This web page presents the results of the 2017 6th International Competition on Software Verification (SV-COMP'17).

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:


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.

ReachSafety
1. SMACK
2. CPA-Seq
3. UAutomizer
Quantile-Plot
MemSafety
1. PredatorHP
2. UAutomizer
3. Symbiotic
Quantile-Plot
ConcurrencySafety
1. Yogar-CBMC
2. Lazy-CSeq-Abs
3. Lazy-CSeq-Swarm
Quantile-Plot
Overflows
1. SMACK
2. UAutomizer
3. UTaipan
Quantile-Plot
Termination
1. UAutomizer
2. AProVE
3. CPA-Seq
Quantile-Plot
SoftwareSystems
1. SMACK
2. UTaipan
3. UAutomizer
Quantile-Plot
FalsificationOverall
1. CBMC
2. ESBMC-kind
3. ESBMC-incr
Quantile-Plot
Overall
1. UAutomizer
2. SMACK
3. CPA-Seq
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.

VerifiersPlots2LSAProVEBLASTCBMCCeagleCIVLConSequenceCPA-BAM-BnBCPA-kIndCPA-SeqDepthKESBMCESBMC-falsiESBMC-incrESBMC-kindForesterHipTNT+Lazy-CSeqLazy-CSeq-AbsLazy-CSeq-SwarmMU-CSeqPredatorHPSkinkSMACKSymbioticSymDIVINEUAutomizerUKojakUL-CSeqUTaipanVeriAbsYogar-CBMC
Representing Jury MemberPeter SchrammelJera HenselVadim MutilinMichael TautschnigGuang ChenStephen SiegelAnand YeolekarPavel AndrianovMatthias DanglKarlheinz FriedbergerHerbert Oliveira RochaLucas CordeiroBernd FischerDenis NicoleMikhail RamalhoMartin HruskaTon Chanh LeOmar InversoBernd FischerTruc Nguyen LamSalvatore La TorreTomas VojnarFranck CassezZvonimir RakamaricJan StrejčekJiří BarnatMatthias HeizmannDaniel DietschGennaro ParlatoMarius GreitschusPriyanka DarkeLiangze Yin
AffiliationUniversity of Sussex, UKRWTH Aachen, GermanyISP RAS, RussiaQueen Mary, UKTsinghua University, ChinaUniversity of Delaware, USATCS, IndiaISP RAS, RussiaUniversity of Passau, GermanyUniversity of Passau, GermanyFederal University of Roraima, BrazilUniversity of Oxford, UKStellenbosch University, ZAUniversity of Southampton, UKUniversity of Southampton, UKBrno University of Technology, CzechiaNational University of Singapore, SingaporeGran Sasso Science Institute, ItalyStellenbosch University, ZAUniversity of Southampton, UKUniversity of Salerno, ItalyBrno University of Technology, CzechiaMacquarie University at Sydney, AustraliaUniversity of Utah, USAMasaryk University, CzechiaMasaryk University, CzechiaUniversity of Freiburg, GermanyUniversity of Freiburg, GermanyUniversity of Southampton, UKUniversity of Freiburg, GermanyTCS, IndiaNational University of Defense Technology, China
ReachSafety
2897 tasks, max. score: 4696
Quantile-Plot 10382154217021562862155211255831810194034322063237215641894
CPU time81000 s32000 s20000 s63000 s140000 s84000 s93000 s27000 s42000 s27000 s360000 s10000 s97000 s64000 s45000 s
ReachSafety-Arrays
135 tasks, max. score: 230
Quantile-Plot -1030214-1048964863630212145221713162
CPU time1200 s1200 s85 s210 s230 s1400 s3000 s23000 s7.5 s490 s660 s8800 s260 s1300 s1300 s210 s45000 s
ReachSafety-BitVectors
50 tasks, max. score: 86
Quantile-Plot 545776-15067755446104853127850562743
CPU time110 s460 s200 s330 s1800 s1700 s3900 s8100 s15 s510 s640 s39 s11000 s780 s2200 s710 s1100 s
ReachSafety-ControlFlow
94 tasks, max. score: 146
Quantile-Plot 44589-180891126427355180125526295477533
CPU time1200 s200 s3000 s1300 s1300 s3100 s4900 s830 s5300 s8100 s9200 s14000 s8.9 s3700 s2900 s4500 s3200 s4700 s
ReachSafety-ECA
1149 tasks, max. score: 1887
Quantile-Plot 644143147463179010883561121118224293-14586159396405
CPU time58000 s24000 s550 s31000 s26000 s86000 s510 s25000 s17000 s26000 s7000 s92000 s8400 s4400 s67000 s46000 s12000 s140000 s
ReachSafety-Floats
172 tasks, max. score: 314
Quantile-Plot 248264298-56107129100308181941731538610962109
CPU time6400 s3000 s15000 s1400 s5700 s4100 s3800 s5200 s2400 s5100 s3300 s5400 s19 s5900 s490 s6400 s
ReachSafety-Heap
173 tasks, max. score: 280
Quantile-Plot -37018669-16017115718413563184148139197272208193152177
CPU time24 s98 s2.8 s720 s780 s1600 s670 s350 s670 s39 s44 s1200 s85 s29000 s29 s3400 s2400 s2600 s
ReachSafety-Loops
156 tasks, max. score: 261
Quantile-Plot 14510733115151157120-29536961189819413660156147162194
CPU time550 s500 s910 s1400 s2300 s5100 s3400 s4500 s390 s190 s1100 s1900 s25000 s29 s330 s1800 s3100 s3100 s8000 s
ReachSafety-ProductLines
597 tasks, max. score: 929
Quantile-Plot 772393134657660920393623129317437920453-592618487562634
CPU time8700 s2300 s10 s4300 s3800 s5800 s50000 s21000 s25 s230 s1800 s160000 s200 s3700 s5200 s3600 s9500 s88000 s
ReachSafety-Recursive
98 tasks, max. score: 151
Quantile-Plot 086431910119357237898912591571166510045
CPU time0 s25 s5.8 s28 s22 s390 s47 s1200 s6.6 s520 s1000 s8400 s8.6 s14 s1800 s670 s4100 s170 s
ReachSafety-Sequentialized
273 tasks, max. score: 376
Quantile-Plot 61360017020633-511376417941-191481512-26
CPU time5000 s230 s0 s2000 s21000 s32000 s14000 s4900 s210 s620 s1900 s12000 s350 s4700 s5200 s1600 s2400 s5800 s
MemSafety
328 tasks, max. score: 541
Quantile-Plot -91821913808827-85-6580191319150304308268296
CPU time440 s1900 s2.5 s0 s1600 s8600 s12000 s4500 s9600 s4800 s2900 s79000 s280 s6800 s7600 s8300 s
MemSafety-Arrays
69 tasks, max. score: 117
Quantile-Plot -4401811600620-3918181878283866484
CPU time4.6 s3.8 s2.5 s0 s0 s14 s11 s8000 s3.4 s3.2 s3.3 s.97 s35000 s55 s860 s2400 s1400 s
MemSafety-Heap
181 tasks, max. score: 272
Quantile-Plot -350190000140-185-41-103-31-437216204202966984
CPU time350 s1400 s0 s0 s0 s890 s6800 s3500 s2400 s6100 s4500 s66 s1600 s26000 s150 s4800 s2700 s5700 s
MemSafety-LinkedLists
52 tasks, max. score: 79
Quantile-Plot -24631000-29151-314154863-1213211108
CPU time27 s530 s0 s0 s0 s130 s68 s39 s1500 s2800 s3.6 s1300 s45 s15000 s32 s1000 s2300 s1000 s
MemSafety-Other
26 tasks, max. score: 49
Quantile-Plot 48200002020-732147364820464646
CPU time57 s31 s0 s0 s0 s580 s1700 s370 s640 s660 s330 s1300 s1700 s41 s150 s200 s150 s
ConcurrencySafety
1047 tasks, max. score: 1293
Quantile-Plot 011351251794010205486015527566541226129312931179-1021208038900117701293
CPU time0 s1800 s14000 s15000 s0 s42000 s100000 s160000 s74000 s87000 s87000 s5900 s7500 s11000 s2000 s90 s77000 s0 s13000 s0 s0 s32000 s0 s1300 s
ConcurrencySafety-Main
1047 tasks, max. score: 1293
Quantile-Plot 01135012517940010205486015527566541226129312931179-1021208038900117701293
CPU time0 s1800 s0 s14000 s15000 s0 s0 s42000 s100000 s160000 s74000 s87000 s87000 s5900 s7500 s11000 s2000 s90 s77000 s0 s13000 s0 s0 s32000 s0 s1300 s
Overflows
328 tasks, max. score: 533
Quantile-Plot 3102301210110185105106187304417281372356365
CPU time48 s210 s1.1 s1300 s1300 s240 s13000 s25 s110 s340 s63000 s340 s3000 s2300 s3100 s
Overflows-BitVectors
274 tasks, max. score: 393
Quantile-Plot 284186200212110269142176279311195328310325
CPU time44 s46 s1.1 s0 s930 s920 s91 s12000 s24 s98 s340 s60000 s63 s2700 s2100 s2800 s
Overflows-Other
54 tasks, max. score: 98
Quantile-Plot 4639002929821727457654585656
CPU time4.0 s160 s0 s0 s360 s360 s150 s910 s.67 s13 s4.2 s3600 s270 s230 s230 s220 s
Termination
1437 tasks, max. score: 2513
Quantile-Plot 62414920974-307000083500218400
CPU time4800 s13000 s0 s49000 s140 s0 s0 s0 s0 s130 s0 s0 s30000 s0 s0 s
Termination-MainControlFlow
247 tasks, max. score: 437
Quantile-Plot 2013910000285000003450039800
CPU time23 s2300 s0 s0 s0 s0 s4000 s0 s0 s0 s0 s0 s60 s0 s0 s2600 s0 s0 s
Termination-MainHeap
262 tasks, max. score: 506
Quantile-Plot -963280000-20-1680000610041300
CPU time120 s7300 s0 s0 s0 s0 s330 s140 s0 s0 s0 s0 s60 s0 s0 s5500 s0 s0 s
Termination-Other
928 tasks, max. score: 1434
Quantile-Plot 79425900008880000010600127400
CPU time4600 s3500 s0 s0 s0 s0 s45000 s0 s0 s0 s0 s0 s11 s0 s0 s22000 s0 s0 s
SoftwareSystems
2871 tasks, max. score: 5520
Quantile-Plot 720866373529757781011254301-1703341695-707910554101067
CPU time6300 s6600 s210 s1500 s12000 s18000 s55000 s21000 s58000 s29 s43 s2400 s73000 s1700 s70000 s100000 s65000 s
Systems_BusyBox_MemSafety
38 tasks, max. score: 72
Quantile-Plot 0010000000006-269000
CPU time0 s0 s9.1 s0 s0 s0 s0 s0 s0 s0 s0 s0 s9600 s25 s0 s0 s0 s
Systems_BusyBox_Overflows
38 tasks, max. score: 76
Quantile-Plot 00000000000023-31222
CPU time0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s880 s0 s10 s15 s10 s
Systems_DeviceDriversLinux64_ReachSafety
2795 tasks, max. score: 5235
Quantile-Plot 21042529351028284822712954741880-50-197528171392-58293410502969
CPU time6300 s6600 s210 s1500 s12000 s18000 s55000 s21000 s58000 s29 s43 s2400 s62000 s1700 s1900 s70000 s100000 s65000 s
FalsificationOverall
7471 tasks, max. score: 2908
Quantile-Plot -43302554343-73523213029761841269148216101154-2698982900918
CPU time38000 s29000 s4500 s23000 s24000 s80000 s65000 s170000 s100000 s120000 s96000 s90000 s9500 s41000 s22000 s23000 s
Overall
8908 tasks, max. score: 14553
Quantile-Plot -1204476619721963529618941674126132094335691742709938374511
CPU time93000 s36000 s22000 s82000 s290000 s220000 s340000 s100000 s140000 s120000 s660000 s12000 s210000 s180000 s120000 s
VerifiersPlots2LSAProVEBLASTCBMCCeagleCIVLConSequenceCPA-BAM-BnBCPA-kIndCPA-SeqDepthKESBMCESBMC-falsiESBMC-incrESBMC-kindForesterHipTNT+Lazy-CSeqLazy-CSeq-AbsLazy-CSeq-SwarmMU-CSeqPredatorHPSkinkSMACKSymbioticSymDIVINEUAutomizerUKojakUL-CSeqUTaipanVeriAbsYogar-CBMC

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.