ETAPS Logo TACAS 2023
12th Competition on Software Verification (SV-COMP 2023)

Results of the Competition

This web page presents the results of SV-COMP 2023 - 12th International Competition on Software Verification.

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)

ReachSafety
1. VeriAbs
2. VeriAbsL
3. PeSCo-CPA
Quantile-Plot
MemSafety
1. Symbiotic
2. CPAchecker
3. UTaipan
Quantile-Plot
ConcurrencySafety
1. Deagle
2. UAutomizer
3. UGemCutter
Quantile-Plot
NoOverflows
1. UAutomizer
2. UTaipan
3. UKojak
Quantile-Plot
Termination
1. VeriFuzz
2. UAutomizer
3. 2LS
Quantile-Plot
SoftwareSystems
1. Symbiotic
2. Bubaak
3. Mopsa
Quantile-Plot
FalsificationOverall
1. Bubaak
2. PeSCo-CPA
3. CPAchecker
Quantile-Plot
Overall
1. UAutomizer
2. PeSCo-CPA
3. CPAchecker
Quantile-Plot
JavaOverall
1. JBMC
2. GDart
3. MLB
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 'Hors Concours' in the row for 'Representing Jury Member' means that the tool was added at the organizer's disposition and does not participate in the rankings or prize allocation.
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.

ParticipantsPlots2LSBRICKBubaakCBMCCoVeriTeam-Verifier-AlgoSelectionCoVeriTeam-Verifier-ParallelPortfolioCPA-BAM-BnBCPA-BAM-SMGCPALockatorCPAcheckerCruxCSeqDartagnanDeagleDIVINEEBFESBMC-incrESBMC-kindFrama-C-SVGazer-ThetaGDart-LLVMGoblintGraves-CPAGraves-ParInferKornLazy-CSeqlf-checkerLocksmithMopsaPeSCo-CPAPICheckerPinakaPredatorHPSymbioticThetaUAutomizerUGemCutterUKojakUTaipanVeriAbsVeriAbsLVeriFuzzVeriOoverCOASTALGDartJava-RangerJayHornJBMCJDartMLBSPF
Representing Jury MemberViktor MalíkLei BuMarek ChalupaMichael TautschnigHors ConcoursHors ConcoursHors ConcoursHors ConcoursHors ConcoursHenrik WachowitzHors ConcoursHors ConcoursHernán Ponce de LeónFei HeHors ConcoursFatimah AljaafariHors ConcoursRafael Sá MenezesMartin SpiesslHors ConcoursFalk HowarSimmo SaanWill LeesonHors ConcursHors ConcoursGidon ErnstHors ConcoursTong WuVesal VojdaniRaphaël MonatCedric RichterJie SuHors ConcoursHors ConcoursMarek TrtikLevente BajcziMatthias HeizmannDominik KlumppFrank SchüsseleDaniel DietschPriyanka DarkePriyanka DarkeRaveendra Kumar MedicherlaHaiPeng QuHors ConcoursFalk HowarSoha HusseinHors ConcoursPeter SchrammelHors ConcoursLei BuHors Concours
AffiliationBrno University of Technology, CzechiaNanjing University, ChinaISTA, AustriaQueen Mary University of London, UK--, ----, ----, ----, ----, --LMU Munich, Germany--, ----, --Huawei Dresden Research Center, GermanyTsinghua University, China--, --University of Manchester, UK--, --University of Manchester, UKLMU Munich, Germany--, --TU Dortmund, GermanyUniversity of Tartu, EstoniaUniversity of Virginia, USAUniversity of Virginia, USA--, --LMU Munich, Germany--, --University of Manchester, UKUniversity of Tartu, EstoniaInria and University of Lille, FranceUniversity of Oldenburg, GermanyXidian University, China--, ----, --Masaryk University, Brno, CzechiaBudapest University of Technology and Economics, HungaryUniversity of Freiburg, GermanyUniversity of Freiburg, GermanyUniversity of Freiburg, GermanyUniversity of Freiburg, GermanyTata Consultancy Services, IndiaTata Consultancy Services, IndiaTata Consultancy Services, IndiaOcean University of China, China--, --TU Dortmund, GermanyUniversity of Minnesota, USA--, --University of Sussex and Diffblue, UK--, --Nanjing University, China--, --
ReachSafety
6138 tasks, max. score: 9814
Quantile-Plot 361742783497-50720335535879269851838744868-64-561296995576338747861076399723063672662864781704
CPU time90000 s130000 s120000 s350000 s310000 s530000 s6900 s130000 s130000 s220 s170000 s34000 s48 s460 s280000 s19000 s100000 s98000 s200000 s99000 s160000 s540000 s420000 s57000 s
ReachSafety-Arrays
300 tasks, max. score: 509
Quantile-Plot 8119149-7416416570-2035100014610-3092683791501174767538134871
CPU time540 s450 s1400 s1700 s9100 s1700 s9100 s96 s1000 s1200 s0 s3.2 s1700 s0 s3.8 s3.1 s2600 s860 s550 s1100 s1700 s1900 s2600 s18000 s14000 s480 s
ReachSafety-BitVectors
49 tasks, max. score: 83
Quantile-Plot 434944394671614442530553220532-654862404728542443696815
CPU time190 s590 s180 s380 s1500 s5300 s3700 s68 s710 s330 s0 s210 s1700 s1.3 s1200 s400 s0.29 s4.0 s2200 s64 s670 s540 s2200 s410 s2200 s2800 s2300 s150 s
ReachSafety-ControlFlow
22 tasks, max. score: 37
Quantile-Plot 246423426-262628240203-240310322191025272731336
CPU time2.5 s27 s27 s130 s810 s2800 s6.2 s120 s68 s3.8 s0 s1000 s190 s0 s190 s0 s480 s0.090 s2400 s870 s680 s990 s410 s1300 s900 s360 s
ReachSafety-ECA
1263 tasks, max. score: 2046
Quantile-Plot 54428030835610571008101431089016106690-127322105326127413278638832812261287390
CPU time68000 s9900 s68000 s81000 s97000 s160000 s320 s49000 s78000 s0 s7600 s0 s50000 s0 s29 s3.4 s130000 s4900 s5400 s39000 s85000 s52000 s22000 s210000 s170000 s29000 s
ReachSafety-Floats
434 tasks, max. score: 824
Quantile-Plot 6057986827547757807065732307503294469960760711770681-424272431789775-6
CPU time3000 s2400 s1700 s7300 s25000 s9000 s6900 s72 s7100 s10000 s280 s2.7 s8500 s9500 s32 s12000 s2300 s850 s4300 s22000 s19 s22000 s16000 s9000 s490 s
ReachSafety-Heap
159 tasks, max. score: 257
Quantile-Plot 85132147135106137-13471995213831-1466621449216621101119816615459
CPU time630 s140 s54 s6800 s660 s2700 s85 s630 s940 s23 s1900 s1700 s3.4 s36 s1900 s5.1 s98 s23 s3000 s5200 s2200 s8900 s4600 s340 s
ReachSafety-Loops
685 tasks, max. score: 1159
Quantile-Plot 423586573520619666486637566052213055312-7508323168636596789473759458738836762198
CPU time8300 s14000 s8000 s25000 s26000 s21000 s820 s17000 s13000 s0 s2000 s20 s15000 s3200 s4.0 s1200 s200 s10000 s3900 s31000 s42000 s29000 s19000 s34000 s47000 s33000 s3300 s
ReachSafety-ProductLines
597 tasks, max. score: 929
Quantile-Plot 706453283351911905247803782067531680902829031314530554272576902911260
CPU time1700 s3500 s420 s19000 s29000 s79000 s3500 s18000 s660 s0 s450 s80 s8100 s0 s150 s15000 s19 s4000 s0 s11000 s7000 s23000 s96000 s56000 s1700 s
ReachSafety-Recursive
59 tasks, max. score: 91
Quantile-Plot 0563851502724454403812280-40479029305613583857504624
CPU time0 s2300 s200 s2100 s750 s380 s27 s810 s2300 s0 s180 s1.3 s480 s0 s1.8 s400 s0 s980 s130 s2100 s370 s2500 s860 s1900 s2100 s4300 s440 s
ReachSafety-Sequentialized
563 tasks, max. score: 736
Quantile-Plot 12338753854564891-2514423780-26562459229332134040-4546351991
CPU time2100 s25000 s2600 s85000 s60000 s110000 s810 s21000 s610 s0.94 s14000 s0 s0 s0.98 s44000 s2300 s10000 s2000 s7700 s9800 s5900 s58000 s63000 s5400 s
ReachSafety-XCSP
114 tasks, max. score: 174
Quantile-Plot 14313615215114914696415014501470-960920140142126114224114914849
CPU time2000 s13000 s750 s7300 s3600 s2700 s140 s700 s1800 s460 s0 s3800 s0 s0 s660 s0 s7600 s1800 s19000 s2000 s8800 s150 s6600 s6100 s3800 s1100 s
ReachSafety-Combinations
671 tasks, max. score: 912
Quantile-Plot 63222215347328303234430100024400304119223269131122188232258
CPU time1500 s31000 s32000 s82000 s75000 s70000 s910 s10000 s21000 s0 s0 s0 s50000 s0 s0 s37000 s2600 s13000 s1200 s13000 s1100 s25000 s65000 s48000 s14000 s
ReachSafety-Hardware
1222 tasks, max. score: 1950
Quantile-Plot 16810034-12590-10293281-832-764214050179-2352-7984569201171551080103158-10425
CPU time2800 s24000 s38 s4100 s2000 s61000 s0 s1000 s860 s0 s87 s16000 s19000 s0 s30 s24000 s3.7 s14000 s3600 s9700 s0 s8800 s8900 s12000 s230 s
MemSafety
3202 tasks, max. score: 4543
Quantile-Plot 611-46551798253925872612-3542000217955619262620230115262354
CPU time460 s6500 s2300 s30000 s20000 s22000 s53 s39000 s92000 s1500 s2100 s5000 s220000 s71000 s120000 s
MemSafety-Arrays
43 tasks, max. score: 63
Quantile-Plot 105324440180412104519412539
CPU time13 s910 s3.4 s110 s16 s17 s0 s3.4 s0 s16 s230 s7.0 s26 s4.5 s250 s980 s620 s920 s
MemSafety-Heap
153 tasks, max. score: 225
Quantile-Plot 151484587143150-7011901489726150165181837880
CPU time110 s660 s570 s2300 s780 s800 s20 s800 s0 s710 s1600 s12 s1100 s1700 s1300 s4900 s5000 s4200 s
MemSafety-LinkedLists
79 tasks, max. score: 131
Quantile-Plot 397980838067425806712267105113444
CPU time330 s72 s240 s1400 s490 s500 s30 s440 s0 s540 s150 s0.96 s610 s54 s1200 s150 s890 s160 s
MemSafety-Other
38 tasks, max. score: 53
Quantile-Plot 292221351922-281902231422354839843
CPU time2.5 s850 s14 s4700 s440 s120 s2.8 s290 s0 s110 s410 s2.4 s160 s320 s2200 s1200 s2500 s1000 s
MemSafety-Juliet
2828 tasks, max. score: 4266
Quantile-Plot 041523560418040214266037270426642351440426600301722213186
CPU time0 s4000 s1400 s21000 s18000 s20000 s0 s38000 s0 s21000 s89000 s1400 s27000 s0 s0 s210000 s59000 s120000 s
MemSafety-MemCleanup
61 tasks, max. score: 62
Quantile-Plot -27-784111154540000430541036414441
CPU time5.7 s0 s5.3 s110 s310 s310 s0 s0 s0 s0 s1300 s0 s450 s2.8 s31 s1900 s3400 s1800 s
ConcurrencySafety
2865 tasks, max. score: 5295
Quantile-Plot 09118559847-27201744-1170212684744-2-31748011621591118-5737-13840102355219412862717271002612
CPU time0 s9.2 s6800 s2200 s74000 s1600 s57000 s55000 s25000 s3800 s31000 s170000 s59000 s91000 s1600 s2800 s920 s30000 s48000 s21000 s10000 s78000 s120000 s130000 s0 s80000 s
ConcurrencySafety-Main
665 tasks, max. score: 999
Quantile-Plot 0247917315-740493604525835-2369-3034682411108-52685184504925241741215796090585
CPU time0 s0.46 s4100 s670 s25000 s380 s25000 s14000 s14000 s460 s31000 s160000 s12000 s2100 s26 s25000 s2600 s4.4 s8000 s5400 s26000 s21000 s10000 s8900 s31000 s26000 s0 s27000 s
ConcurrencySafety-MemSafety
705 tasks, max. score: 1410
Quantile-Plot 02042840-16-434001316002984300-16-16266-4384268-1624803323380338
CPU time0 s0.48 s0 s110 s24000 s0 s0 s14000 s0 s960 s0 s0 s22000 s41000 s0 s0 s0 s450 s7300 s17000 s0 s0.57 s24000 s7600 s10000 s0 s7400 s
ConcurrencySafety-NoOverflows
712 tasks, max. score: 1417
Quantile-Plot 05665362180858-44040139200208350308418680-444826485854781058103501072
CPU time0 s8.3 s2700 s1400 s25000 s0 s12000 s13000 s0 s230 s0 s0 s25000 s48000 s160 s27 s220 s220 s7300 s26000 s13000 s4.8 s28000 s28000 s31000 s0 s25000 s
NoDataRace-Main
783 tasks, max. score: 1488
Quantile-Plot 0400-38407681211130402262057567320612
CPU time0 s20000 s14000 s12000 s2200 s1400 s0 s15 s17000 s55000 s62000 s0 s21000 s
NoOverflows
6618 tasks, max. score: 10200
Quantile-Plot 657050056267-3793407913160634215225306-17785-772205671-8792407863973058492-500
CPU time3200 s28000 s23000 s30000 s4600 s3500 s0 s17000 s3500 s530 s1600 s1300 s3800 s160 s1800 s190000 s120000 s200000 s1300 s
NoOverflows-Main
576 tasks, max. score: 917
Quantile-Plot 6123203517317102290350-14840270757-6284422710-153419758654752-87-560
CPU time440 s1500 s230 s3900 s4600 s3500 s0 s380 s33 s40 s4600 s1600 s75 s260 s5700 s160 s1800 s13000 s10000 s13000 s1300 s0 s
NoOverflows-Juliet
6042 tasks, max. score: 9006
Quantile-Plot 557657827761-145940007908433254720-33072-7508259280007824647876180
CPU time2700 s26000 s23000 s26000 s0 s0 s0 s16000 s3500 s480 s0 s0 s1200 s3500 s0 s0 s0 s180000 s110000 s180000 s0 s
Termination
1809 tasks, max. score: 3103
Quantile-Plot 118319586294788307825906319302105002305
CPU time13000 s26000 s9600 s18000 s35000 s0 s3900 s12000 s630 s14000 s47000 s0 s0 s76000 s
Termination-BitVectors
34 tasks, max. score: 57
Quantile-Plot 2832262770240-1212072626390046
CPU time3.7 s56 s4.4 s74 s17 s0 s4.7 s0 s24 s210 s28 s3.1 s34 s540 s0 s0 s41 s
Termination-MainControlFlow
277 tasks, max. score: 488
Quantile-Plot 2567664292830640180212283566237900340
CPU time55 s3300 s55 s1900 s1800 s0 s950 s0 s2800 s3200 s2200 s72 s79 s5100 s0 s0 s910 s
Termination-MainHeap
37 tasks, max. score: 70
Quantile-Plot 0-622200200-14022430054
CPU time0 s3.7 s0.34 s2.9 s0 s0 s0.24 s0 s0 s28 s0 s0.084 s0.46 s1200 s0 s0 s140 s
Termination-Other
1461 tasks, max. score: 2237
Quantile-Plot 126813031250166710600108001187482106054814811428001545
CPU time13000 s23000 s9500 s16000 s33000 s0 s3000 s0 s54000 s8800 s35000 s560 s14000 s40000 s0 s0 s75000 s
SoftwareSystems
3173 tasks, max. score: 5132
Quantile-Plot 751589-7111421458804758101275358-1186-1337-255568158121604476274412
CPU time58 s1100 s4300 s92000 s80000 s85000 s160000 s8900 s24000 s30000 s77000 s54000 s250 s43000 s170000 s2900 s120000 s59000 s110000 s
SoftwareSystems-AWS-C-Common-ReachSafety
165 tasks, max. score: 323
Quantile-Plot 22163-1205702075-39981936628326017770434
CPU time5.7 s220 s120 s2800 s1100 s410 s250 s2800 s73 s220 s250 s5.5 s3100 s190 s18 s5100 s270 s3800 s66 s1600 s
SoftwareSystems-BusyBox-ReachSafety
5 tasks, max. score: 5
Quantile-Plot 00000000000-32-320010000
CPU time0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s57 s0 s0 s0 s0 s
SoftwareSystems-BusyBox-MemSafety
31 tasks, max. score: 55
Quantile-Plot 05-6200000000-379004000
CPU time0 s28 s71 s0 s0 s0 s0 s0 s0 s0 s0 s14 s0 s0 s51 s0 s0 s0 s
SoftwareSystems-BusyBox-NoOverflows
58 tasks, max. score: 83
Quantile-Plot 0-1500004-32000042-558440444
CPU time0 s260 s0 s0 s0 s0 s1200 s0 s0 s0 s0 s0 s1100 s510 s0.37 s2.1 s1200 s0 s120 s170 s530 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety
2418 tasks, max. score: 4597
Quantile-Plot 30475-51297412497323132332760-22428728189824762960818317429521350277420432767
CPU time53 s140 s190 s66000 s86000 s80000 s84000 s150000 s43 s8700 s23000 s30000 s72000 s51000 s43000 s160000 s1600 s120000 s59000 s110000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety
8 tasks, max. score: 16
Quantile-Plot 00000220-96000001000000
CPU time0 s0 s0 s0 s0 s330 s320 s0 s0 s0 s0 s0 s0 s0 s20 s0 s0 s0 s0 s0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety
94 tasks, max. score: 94
Quantile-Plot 0433250362505-714025-31111
CPU time0 s130 s48 s530 s0 s440 s290 s0 s680 s280 s540 s0 s350 s31 s51 s34 s50 s
SoftwareSystems-OpenBSD-MemSafety
4 tasks, max. score: 5
Quantile-Plot 04420000002-15004000
CPU time0 s6.2 s2.5 s58 s0 s0 s0 s0 s0 s0 s15 s4.5 s0 s0 s56 s0 s0 s0 s
SoftwareSystems-uthash-MemSafety
138 tasks, max. score: 204
Quantile-Plot 02049615609696009696-2172096204000
CPU time0 s250 s3900 s3600 s0 s520 s530 s0 s0 s640 s1900 s180 s0 s650 s810 s0 s0 s0 s
SoftwareSystems-uthash-NoOverflows
114 tasks, max. score: 228
00000000000000-480000000
CPU time0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s
SoftwareSystems-uthash-ReachSafety
138 tasks, max. score: 276
Quantile-Plot 0228002280006000000-220800228000
CPU time0 s110 s0 s0 s880 s0 s0 s0 s8.1 s0 s0 s0 s0 s0 s0 s0 s0 s79 s0 s0 s0 s
FalsificationOverall
21996 tasks, max. score: 8689
Quantile-Plot 18844313211037344254-57335073447-306342584026417330924100
CPU time30000 s130000 s110000 s240000 s320000 s120000 s78000 s170000 s65000 s170000 s55000 s220000 s79000 s170000 s
Overall
23805 tasks, max. score: 38644
Quantile-Plot 972224261088672121455914291329963975258-8217146521209719589810214514
CPU time110000 s190000 s170000 s560000 s810000 s170000 s310000 s32000 s360000 s200000 s580000 s140000 s890000 s350000 s670000 s
JavaOverall
586 tasks, max. score: 827
Quantile-Plot -2816652400220667382495182
CPU time710 s11000 s14000 s5500 s1200 s1800 s1400 s1400 s
ReachSafety-Java
586 tasks, max. score: 827
Quantile-Plot -2816652400220667382495182
CPU time710 s11000 s14000 s5500 s1200 s1800 s1400 s1400 s
ParticipantsPlots2LSBRICKBubaakCBMCCoVeriTeam-Verifier-AlgoSelectionCoVeriTeam-Verifier-ParallelPortfolioCPA-BAM-BnBCPA-BAM-SMGCPALockatorCPAcheckerCruxCSeqDartagnanDeagleDIVINEEBFESBMC-incrESBMC-kindFrama-C-SVGazer-ThetaGDart-LLVMGoblintGraves-CPAGraves-ParInferKornLazy-CSeqlf-checkerLocksmithMopsaPeSCo-CPAPICheckerPinakaPredatorHPSymbioticThetaUAutomizerUGemCutterUKojakUTaipanVeriAbsVeriAbsLVeriFuzzVeriOoverCOASTALGDartJava-RangerJayHornJBMCJDartMLBSPF

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.


If you did not find what you are looking for, please do not hesitate to contact Dirk Beyer (competition chair).

Imprint and Privacy Policy