TACAS Logo TACAS 2018
7th Competition on Software Verification (SV-COMP)

Results of the Competition

This web page presents the results of the 2018 7th 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. CPA-Seq
2. VeriAbs
3. UAutomizer
Quantile-Plot
MemSafety
1. Symbiotic
2. PredatorHP
3. UKojak
Quantile-Plot
ConcurrencySafety
1. Yogar-CBMC
2. CPA-Seq
3. CBMC
Quantile-Plot
NoOverflows
1. UAutomizer
2. CPA-Seq
3. UTaipan
Quantile-Plot
Termination
1. UAutomizer
2. AProVE
3. CPA-Seq
Quantile-Plot
SoftwareSystems
1. CPA-BAM-BnB
2. UAutomizer
3. CPA-BAM-Slicing
Quantile-Plot
FalsificationOverall
1. CPA-Seq
2. CBMC
3. Symbiotic
Quantile-Plot
Overall
1. CPA-Seq
2. UAutomizer
3. ESBMC-kind
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.

VerifiersPlots2LSAProVECBMCCPA-BAM-BnBCPA-BAM-SlicingCPA-SeqDepthKESBMC-incrESBMC-kindForesterInterpCheckerMap2CheckPredatorHPSkinkSymbioticUAutomizerUKojakUTaipanVeriAbsVIAPYogar-CBMC
Representing Jury MemberPeter SchrammelJera HenselMichael TautschnigVadim MutilinMikhail MandrykinThomas LembergerHussama IsmailFelipe MonteiroMikhail R. GadelhaMartin HruskaZhao DuanHerbert Oliveira RochaVeronika ŠokováFranck CassezMarek ChalupaMatthias HeizmannAlexander NutzDaniel DietschPriyanka DarkePritom RajkhowaLiangze Yin
AffiliationUniversity of SussexRWTH Aachen UniversityQueen Mary University of LondonISP RASISP RASLMU MunichFederal University of AmazonasFederal University of AmazonasUniversity of SouthamptonBrno University of TechnologyXidian UniversityFederal University of RoraimaBUT, Brno, Czech RepublicMacquarie UniversityFaculty of Informatics of Masaryk University, BrnoUniversity of FreiburgUniversity of FreiburgUniversity of FreiburgTata Consultancy ServicesThe Hong Kong University of Science and TechnologyNational University of Defense Technology
ReachSafety
2941 tasks, max. score: 4775
Quantile-Plot 201621173058159421062363-8183-207118122272475161919692760726
CPU time79000 s33000 s180000 s150000 s44000 s47000 s87000 s4100 s2800 s21000 s110000 s58000 s71000 s170000 s7900 s
ReachSafety-Arrays
167 tasks, max. score: 290
Quantile-Plot -5526-297-7581633438-5453452146161518235209
CPU time600 s1000 s47 s340 s1700 s1300 s570 s580 s2400 s1700 s480 s350 s390 s380 s150 s10000 s7000 s
ReachSafety-BitVectors
50 tasks, max. score: 86
Quantile-Plot 5649-155-14977535656-508-68365458335653
CPU time98 s560 s170 s320 s1600 s3900 s330 s350 s710 s880 s180 s1400 s1800 s1600 s3200 s1100 s
ReachSafety-ControlFlow
94 tasks, max. score: 146
Quantile-Plot 6359-190104108614570-51226297444651
CPU time150 s310 s920 s1200 s1900 s1800 s150 s180 s3300 s46 s13 s4500 s2500 s8000 s3700 s
ReachSafety-ECA
1148 tasks, max. score: 1886
Quantile-Plot 72414277049211798930530336575792345184918
CPU time64000 s25000 s80000 s15000 s120000 s40000 s35000 s37000 s58000 s6800 s76000 s39000 s24000 s82000 s
ReachSafety-Floats
172 tasks, max. score: 313
Quantile-Plot 251259-714-23518154257263-1424918313193131202
CPU time4800 s3100 s310 s420 s6000 s2800 s5100 s5500 s560 s370 s18 s4100 s610 s4200 s9200 s
ReachSafety-Heap
181 tasks, max. score: 291
Quantile-Plot 108192-1687119316317419113911346203135201200186157129
CPU time13 s170 s500 s780 s4200 s1000 s41 s44 s1300 s1200 s75 s81 s510 s24 s2200 s3200 s3300 s1700 s
ReachSafety-Loops
163 tasks, max. score: 274
Quantile-Plot 139106137591781199113413-13415415218915919121644
CPU time690 s570 s1700 s1700 s4900 s3400 s2000 s1900 s1800 s1200 s860 s520 s2300 s2400 s2900 s6500 s210 s
ReachSafety-ProductLines
597 tasks, max. score: 929
Quantile-Plot 795301711663919443453573203461626440529513
CPU time7800 s660 s20000 s4100 s7000 s69000 s710 s1100 s9900 s200 s7700 s4300 s19000 s31000 s
ReachSafety-Recursive
96 tasks, max. score: 148
Quantile-Plot 095-630-640108429999-6369851103116611048191
CPU time0 s460 s160 s120 s490 s560 s380 s420 s130 s290 s400 s12 s1800 s840 s5000 s4900 s650 s
ReachSafety-Sequentialized
273 tasks, max. score: 376
Quantile-Plot 143164-364101941347977-86143421913180
CPU time1700 s1600 s2600 s2000 s26000 s22000 s480 s490 s9500 s12000 s5700 s3000 s1400 s22000 s
MemSafety
326 tasks, max. score: 539
Quantile-Plot 169132181-2811523883022828604112542652490
CPU time130 s1800 s1700 s3400 s1400 s1300 s1300 s0 s4000 s2100 s0 s310 s5200 s11000 s3200 s0 s
MemSafety-Arrays
69 tasks, max. score: 117
Quantile-Plot 120061314151067105427053
CPU time.24 s8.0 s0 s0 s15 s6.7 s3.4 s3.8 s2300 s.96 s23 s240 s3100 s600 s
MemSafety-Heap
180 tasks, max. score: 270
Quantile-Plot 4612300183-23411312935174201199876978
CPU time120 s1600 s0 s0 s650 s2800 s1400 s1300 s67 s1400 s1600 s71 s3000 s5900 s2100 s
MemSafety-LinkedLists
51 tasks, max. score: 78
Quantile-Plot 21100164-611421150271344
CPU time.77 s200 s0 s0 s77 s3.2 s3.7 s4.0 s1300 s14 s39 s57 s1800 s1500 s360 s
MemSafety-Other
26 tasks, max. score: 49
Quantile-Plot 4618002118184623449464646
CPU time7.3 s9.1 s0 s0 s920 s600 s2.6 s4.4 s310 s400 s150 s120 s180 s120 s
ConcurrencySafety
1047 tasks, max. score: 1293
Quantile-Plot 076596910345333000000001266
CPU time0 s1300 s42000 s59000 s67000 s67000 s0 s0 s0 s0 s0 s0 s0 s0 s1100 s
ConcurrencySafety-Main
1047 tasks, max. score: 1293
Quantile-Plot 07650-240389691034533300001266
CPU time0 s1300 s0 s860 s42000 s59000 s67000 s67000 s0 s0 s0 s0 s1100 s
NoOverflows
358 tasks, max. score: 574
Quantile-Plot 281214436-1012213280-26303244474084270
CPU time91 s100 s2000 s150 s92 s89 s0 s220 s0 s98 s2500 s2400 s2200 s0 s
NoOverflows-BitVectors
280 tasks, max. score: 402
Quantile-Plot 27418800313-3218829788195351318319
CPU time87 s88 s0 s0 s1200 s0 s64 s81 s94 s42 s2200 s2100 s1900 s
NoOverflows-Other
78 tasks, max. score: 138
Quantile-Plot 464100103-354460-13987978997
CPU time4.1 s16 s0 s0 s840 s150 s28 s8.2 s120 s56 s310 s290 s300 s
Termination
2009 tasks, max. score: 3528
Quantile-Plot 152223178251628-27482482400003022000
CPU time9800 s64000 s4400 s58000 s290 s3000 s3000 s0 s0 s0 s0 s37000 s0 s0 s0 s
Termination-MainControlFlow
250 tasks, max. score: 444
Quantile-Plot 269376600029106060039700
CPU time73 s2000 s66 s0 s0 s2400 s0 s270 s260 s0 s2400 s0 s0 s
Termination-MainHeap
260 tasks, max. score: 503
Quantile-Plot 100336240067-1362424040900
CPU time31 s6800 s66 s0 s0 s6900 s140 s610 s610 s0 s4600 s0 s0 s
Termination-Other
1499 tasks, max. score: 2336
Quantile-Plot 12189951348001513170134613460202500
CPU time9700 s55000 s4300 s0 s0 s48000 s160 s2200 s2200 s0 s30000 s0 s0 s
SoftwareSystems
2842 tasks, max. score: 5014
Quantile-Plot 102-11127010501018255-2477975300571116372710500
CPU time26 s290 s39000 s10000 s68000 s20000 s1100 s12000 s18000 s0 s0 s2000 s110000 s160000 s110000 s0 s
Systems_BusyBox_MemSafety
38 tasks, max. score: 72
Quantile-Plot 0000001101000
CPU time0 s0 s0 s0 s0 s0 s780 s400 s0 s2.0 s0 s0 s0 s
Systems_BusyBox_NoOverflows
70 tasks, max. score: 107
Quantile-Plot 0000000000444
CPU time0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s23 s47 s23 s
Systems_DeviceDriversLinux64_ReachSafety
2734 tasks, max. score: 5112
Quantile-Plot 295-31366530302937735-142217621721575320019412873
CPU time26 s290 s39000 s10000 s68000 s20000 s320 s12000 s18000 s2000 s110000 s160000 s110000 s
FalsificationOverall
7514 tasks, max. score: 3189
Quantile-Plot 67816112213-83111461307-4225143911461100089287293
CPU time41000 s29000 s100000 s80000 s64000 s67000 s26000 s1200 s550 s21000 s45000 s22000 s27000 s1000 s
Overall
9523 tasks, max. score: 15291
Quantile-Plot 44174541779221938355476-3996-1676374959759043744750392
CPU time89000 s41000 s350000 s230000 s120000 s130000 s100000 s8300 s2800 s23000 s260000 s230000 s190000 s7900 s
VerifiersPlots2LSAProVECBMCCPA-BAM-BnBCPA-BAM-SlicingCPA-SeqDepthKESBMC-incrESBMC-kindForesterInterpCheckerMap2CheckPredatorHPSkinkSymbioticUAutomizerUKojakUTaipanVeriAbsVIAPYogar-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.