TACAS Logo TACAS 2019
8th Competition on Software Verification (SV-COMP)

Results of the Competition

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:


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. VeriAbs
2. CPA-Seq
3. PeSCo
Quantile-Plot
MemSafety
1. Symbiotic
2. PredatorHP
3. CPA-Seq
Quantile-Plot
ConcurrencySafety
1. Yogar-CBMC
2. Lazy-CSeq
3. CPA-Seq
Quantile-Plot
NoOverflows
1. UAutomizer
2. UTaipan
3. CPA-Seq
Quantile-Plot
Termination
1. UAutomizer
2. AProVE
3. CPA-Seq
Quantile-Plot
SoftwareSystems
1. CPA-BAM-BnB
2. CPA-Seq
3. VeriAbs
Quantile-Plot
FalsificationOverall
1. CPA-Seq
2. PeSCo
3. ESBMC-kind
Quantile-Plot
Overall
1. CPA-Seq
2. PeSCo
3. UAutomizer
Quantile-Plot
JavaOverall
1. JBMC
2. SPF
3. JPF
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.

VerifiersPlots2LSAProVECBMCCBMC-PathCPA-BAM-BnBCPA-LockatorCPA-SeqDepthKDIVINE-explicitDIVINE-SMTESBMC-kindJayHornJBMCJPFLazy-CSeqMap2CheckPeSCoPinakaPredatorHPSkinkSMACKSPFSymbioticUAutomizerUKojakUTaipanVeriAbsVeriFuzzVIAPYogar-CBMCYogar-CBMC-Parallel
Representing Jury MemberPeter SchrammelJera HenselMichael TautschnigKareem KhazemVadim MutilinPavel AndrianovMarie-Christine JakobsOmar AlhawiVladimír ŠtillHenrich LaukoMikhail R. GadelhaPhilipp RuemmerLucas CordeiroCyrille ArthoOmar InversoHerbert RochaCedric RichterEti ChaudharyVeronika ŠokováFranck CassezZvonimir RakamaricWillem VisserMarek ChalupaMatthias HeizmannAlexander NutzDaniel DietschPriyanka DarkeRaveendra Kumar MedicherlaPritom RajkhowaLiangze YinHaining Feng
AffiliationUniversity of Sussex, UKRWTH Aachen, GermanyAmazon Web Services, UKUniversity College London, UKISP RAS, RussiaISP RAS, RussiaLMU Munich, GermanyUniversity of Manchester, UKMasaryk University, CzechiaMasaryk University, CzechiaUniversity of Southampton, UKUppsala University, SwedenUniversity of Manchester, UKKTH, DenmarkGran Sasso Science Institute, ItalyFederal University of Roraima, BrazilUniversity of Paderborn, GermanyIIT Hyderabad, IndiaBUT, Brno, CzechiaMacquarie University, AustraliaUniversity of Utah, USAStellenbosch University, South AfricaMasaryk University, CzechiaUniversity of Freiburg, GermanyUniversity of Freiburg, GermanyUniversity of Freiburg, GermanyTata Consultancy Services, IndiaTCS Research, IndiaHong Kong University of Science and Technology, ChinaNational University of Defense Technology, ChinaNational University of Defense Technology, China
ReachSafety
3831 tasks, max. score: 6296
Quantile-Plot 23972781165742999861413177834044239 *)314332642195301246381132
CPU time60000 s33000 s20000 s220000 s49000 s6500 s43000 s90000 s210000 s25000 s150000 s120000 s180000 s400000 s85000 s
ReachSafety-Arrays
231 tasks, max. score: 418
Quantile-Plot -29321911-11352317251294921018181836533378
CPU time37 s640 s620 s720 s72 s420 s1500 s960 s790 s910 s8100 s380 s1300 s150 s1300 s170 s4300 s340 s9000 s
ReachSafety-BitVectors
50 tasks, max. score: 86
Quantile-Plot 535022751117265712724037506237625713
CPU time110 s330 s22 s1300 s40 s89 s280 s310 s150 s1100 s91 s230 s100 s2800 s1200 s3100 s2400 s370 s
ReachSafety-ControlFlow
94 tasks, max. score: 146
Quantile-Plot 596212126360283-591292624608443496720
CPU time87 s340 s210 s4100 s840 s0 s1000 s480 s7.4 s3300 s48 s58 s18 s3500 s4300 s3500 s5300 s640 s
ReachSafety-ECA
1256 tasks, max. score: 2041
Quantile-Plot 60413041099144021113978261828353497731515430
CPU time48000 s21000 s110 s110000 s41000 s0 s1600 s78000 s99000 s19000 s2800 s85000 s56000 s110000 s120000 s55000 s
ReachSafety-Floats
469 tasks, max. score: 893
Quantile-Plot 7218007927613644242679073780753168845963543863582343
CPU time2700 s6100 s7900 s11000 s980 s2300 s2200 s7600 s20000 s1500 s3800 s25000 s55 s30000 s31000 s31000 s32000 s910 s
ReachSafety-Heap
241 tasks, max. score: 407
Quantile-Plot 141288233293188221252300-728223626213829820422216530566
CPU time150 s190 s8200 s3100 s960 s1400 s1600 s270 s1400 s4800 s79 s67 s580 s43 s4000 s3400 s4300 s11000 s500 s
ReachSafety-Loops
208 tasks, max. score: 357
Quantile-Plot 140136652263885123130-792249519018021222422227548178
CPU time500 s1200 s150 s7000 s86 s1100 s2200 s1700 s1300 s4800 s570 s1600 s180 s3700 s4700 s3700 s12000 s200 s3500 s
ReachSafety-ProductLines
597 tasks, max. score: 929
Quantile-Plot 732284134918265134248787909314898453630308612904265
CPU time6900 s500 s2100 s7400 s1200 s690 s16000 s600 s39000 s1000 s150000 s280 s9200 s5000 s14000 s95000 s2700 s
ReachSafety-Recursive
96 tasks, max. score: 148
Quantile-Plot 09945111368199993711299531021206211310743124
CPU time0 s310 s1100 s1200 s57 s450 s1300 s370 s48 s2100 s530 s420 s17 s3000 s1100 s5200 s7800 s1500 s710 s
ReachSafety-Sequentialized
589 tasks, max. score: 778
Quantile-Plot 1131757494270-70-36505401406704859292300
CPU time2100 s2500 s19 s69000 s4200 s0 s15000 s280 s34000 s21000 s21000 s12000 s9800 s9900 s110000 s23000 s
MemSafety
434 tasks, max. score: 649
Quantile-Plot 12960-59349-11325-158-20838416 *)426-163-211-91
CPU time470 s1600 s7700 s2000 s2800 s1500 s1600 s1800 s16000 s2200 s110 s8300 s13000 s8300 s
MemSafety-Arrays
71 tasks, max. score: 120
Quantile-Plot 0412420161891-44141410369101
CPU time0 s13 s1.1 s11 s5.0 s8.3 s51 s2.5 s4300 s11 s2.6 s5.6 s1300 s2100 s1600 s
MemSafety-Heap
180 tasks, max. score: 270
Quantile-Plot 5611694183-950-125120140183204194738473
CPU time280 s1200 s71 s760 s1900 s690 s720 s1300 s7500 s770 s960 s36 s3400 s7400 s5200 s
MemSafety-LinkedLists
103 tasks, max. score: 178
Quantile-Plot -20555411450884110711211414812112621116
CPU time150 s360 s7500 s600 s800 s700 s720 s460 s3300 s580 s33 s11000 s33 s3100 s2500 s940 s
MemSafety-Other
48 tasks, max. score: 75
Quantile-Plot 49-26-9142-26-28-77-209-13042585269313
CPU time7.9 s24 s110 s470 s2.9 s130 s120 s25 s700 s460 s1200 s1900 s25 s550 s980 s550 s
MemSafety-MemCleanup
32 tasks, max. score: 32
Quantile-Plot 110031-3200000262831-128-128-96
CPU time37 s0 s0 s130 s0 s0 s0 s0 s0 s0 s7.9 s110 s7.9 s0 s0 s0 s
ConcurrencySafety
1082 tasks, max. score: 1344
Quantile-Plot 0613-150-4419964204933394041245 *)027002711277
CPU time0 s1700 s1100 s1200 s48000 s4500 s7800 s23000 s3300 s11000 s0 s2500 s0 s3400 s1100 s
ConcurrencySafety-Main
1082 tasks, max. score: 1344
Quantile-Plot 0613-150-44199642049333940412459370270027112771273
CPU time0 s1700 s1100 s1200 s48000 s4500 s7800 s23000 s3300 s11000 s55000 s0 s2500 s0 s3400 s1100 s3200 s
NoOverflows
359 tasks, max. score: 574
Quantile-Plot 28022719243139002248218 *)331449396438123
CPU time96 s56 s140 s2100 s3.4 s0 s0 s68 s2300 s160 s260 s3400 s3400 s3400 s5300 s
NoOverflows-BitVectors
280 tasks, max. score: 402
Quantile-Plot 27319116131100018712311177204350309346131
CPU time92 s51 s130 s1200 s0 s0 s0 s42 s470 s1200 s64 s52 s2800 s2900 s2800 s5300 s
NoOverflows-Other
79 tasks, max. score: 139
Quantile-Plot 4646391021700460102468899879517
CPU time4.0 s4.8 s12 s870 s3.4 s0 s0 s26 s1800 s860 s93 s210 s610 s440 s590 s68 s
Termination
2007 tasks, max. score: 3529
Quantile-Plot 1279247682753517853700826561 *)1153300100
CPU time7300 s120000 s4400 s2600 s56000 s180 s0 s0 s2800 s2700 s8800 s46000 s0 s0 s
Termination-MainControlFlow
249 tasks, max. score: 443
Quantile-Plot 2753976048320000602905215440100
CPU time51 s2800 s20 s12 s2800 s0 s0 s0 s210 s2800 s19 s710 s3100 s0 s0 s
Termination-MainHeap
259 tasks, max. score: 502
Quantile-Plot -263402422650002459227240500
CPU time4.2 s6100 s16 s13 s4700 s110 s0 s0 s510 s4400 s120 s10 s4900 s0 s0 s
Termination-Other
1499 tasks, max. score: 2335
Quantile-Plot 13611189135278216968400135015828161240196700
CPU time7200 s110000 s4400 s2600 s48000 s73 s0 s0 s2000 s41000 s2600 s8100 s38000 s0 s0 s
SoftwareSystems
2809 tasks, max. score: 4955
Quantile-Plot 1190-15111851073-118220714 *)55510208189621061
CPU time180 s600 s360 s33000 s99000 s0 s17 s0 s20000 s250 s92000 s63000 s61000 s87000 s
Systems_BusyBox_MemSafety
40 tasks, max. score: 76
Quantile-Plot 00000-32001010000
CPU time0 s0 s0 s0 s0 s0 s0 s0 s540 s0 s.65 s0 s0 s0 s0 s
Systems_BusyBox_NoOverflows
71 tasks, max. score: 108
Quantile-Plot 00000-32000002220
CPU time0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s18 s33 s19 s0 s
Systems_DeviceDriversLinux64_ReachSafety
2698 tasks, max. score: 5046
Quantile-Plot 3430-43434153093-32601990293315322862228026953056
CPU time180 s600 s360 s33000 s99000 s0 s17 s0 s20000 s100000 s250 s92000 s63000 s61000 s87000 s
FalsificationOverall
8515 tasks, max. score: 3843
Quantile-Plot 7331432812823129200-33919162313 *)1828105010601024
CPU time22000 s27000 s5200 s140000 s51000 s4800 s47000 s53000 s190000 s23000 s59000 s35000 s56000 s
Overall
10522 tasks, max. score: 16663
Quantile-Plot 4174434115879329159154772636368466 *)6129672725954188
CPU time68000 s41000 s32000 s420000 s57000 s16000 s67000 s120000 s420000 s35000 s310000 s200000 s260000 s
JavaOverall
368 tasks, max. score: 532
Quantile-Plot 247470290365
CPU time2100 s9700 s550 s970 s
ReachSafety-Java
368 tasks, max. score: 532
Quantile-Plot 247470290365
CPU time2100 s9700 s550 s970 s
VerifiersPlots2LSAProVECBMCCBMC-PathCPA-BAM-BnBCPA-LockatorCPA-SeqDepthKDIVINE-explicitDIVINE-SMTESBMC-kindJayHornJBMCJPFLazy-CSeqMap2CheckPeSCoPinakaPredatorHPSkinkSMACKSPFSymbioticUAutomizerUKojakUTaipanVeriAbsVeriFuzzVIAPYogar-CBMCYogar-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.