ETAPS Logo TACAS 2024
13th Competition on Software Verification (SV-COMP 2024)

Results of the Competition

This web page presents the results of SV-COMP 2024 - 13th 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. VeriAbsL
2. VeriAbs
3. CPAchecker
Quantile-Plot
MemSafety
1. PredatorHP
2. Symbiotic
3. UAutomizer
Quantile-Plot
ConcurrencySafety
1. Dartagnan
2. UGemCutter
3. UAutomizer
Quantile-Plot
NoOverflows
1. UAutomizer
2. UTaipan
3. CPAchecker
Quantile-Plot
Termination
1. PROTON
2. UAutomizer
3. 2LS
Quantile-Plot
SoftwareSystems
1. Mopsa
2. Bubaak-SpLit
3. CPAchecker
Quantile-Plot
FalsificationOverall
1. CPAchecker
2. Symbiotic
3. UTaipan
Quantile-Plot
Overall
1. UAutomizer
2. CPAchecker
3. UTaipan
Quantile-Plot
JavaOverall
1. MLB
2. JBMC
3. GDart
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.

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 Deagle has been disqualified from several categories because the verifier uses identifiers contained in the verification task to identify groups of tasks to set parameters of the verification engine. More precisely: (a) Deagle identifies the presence of variables named “threads_total” here. (b) In such cases, it uses a special unwinding limit here. (c) In such cases, it does not generate unwinding assumptions here and here.

ParticipantsPlots2LSaiseBRICKBubaakBubaak-SpLitCBMCCoVeriTeam-Verifier-AlgoSelectionCoVeriTeam-Verifier-ParallelPortfolioCPA-BAM-BnBCPA-BAM-SMGCPALockatorCPAcheckerCPVCruxCSeqDartagnanDeagleDIVINEEBFEmergenThetaESBMC-incrESBMC-kindFrama-C-SVGazer-ThetaGDart-LLVMGoblintGraves-CPAGraves-ParInferKornLazy-CSeqLF-checkerLocksmithMopsaPeSCo-CPAPICheckerPinakaPredatorHPPROTONsv-sanitizersSymbioticThetaUAutomizerUGemCutterUKojakUTaipanVeriAbsVeriAbsLVeriOoverCOASTALGDartJava-RangerJayHornJBMCJDartMLBSPFSWAT
Representing Jury MemberViktor MalíkZhenbang ChenLei BuMarek ChalupaMarek ChalupaHors ConcoursHors ConcoursHors ConcoursHors ConcoursHors ConcoursHors ConcoursDaniel BaierPo-Chun ChienHors ConcoursHors ConcoursHernán Ponce de LeónFei HeHors ConcoursFatimah AljaafariLevente BajcziHors ConcoursFranz BraußeMartin SpiesslHors ConcoursHors ConcoursSimmo SaanHors ConcoursHors ConcoursHors ConcoursGidon ErnstHors ConcoursHors ConcoursHors ConcoursRaphaël MonatHors ConcoursHors ConcoursHors ConcoursVeronika ŠokováRavindra MettaSimmo SaanMartin JonášLevente BajcziMatthias HeizmannDominik KlumppFrank SchüsseleDaniel DietschPriyanka DarkePriyanka DarkeHors ConcoursHors ConcoursFalk HowarHors ConcoursHassan MousaviPeter SchrammelHors ConcoursLei BuHors ConcoursNils Loose
AffiliationBrno University of Technology, CzechiaNational University of Defense Technology, ChinaNanjing University, ChinaISTA, AustriaISTA, Austria--, ----, ----, ----, ----, ----, --LMU Munich, GermanyLMU Munich, Germany--, ----, --Huawei Dresden Research Center, GermanyTsinghua University, China--, --University of Manchester, UKBudapest University of Technology and Economics, Hungary--, --University of Manchester, UKLMU Munich, Germany--, ----, --University of Tartu, Estonia--, --University of Virginia, USA--, --LMU Munich, Germany--, ----, ----, --Inria and University of Lille, France--, ----, ----, --Brno University of Technology, CzechiaTCS, IndiaUniversity of Tartu, EstoniaMasaryk 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, India--, ----, --TU Dortmund, Germany--, --University of Tehran, Tehran Institute for Advanced Studies, IranUniversity of Sussex and Diffblue, UK--, --Nanjing University, China--, --University of Luebeck, Germany
ReachSafety
11222 valid tasks (8323 true, 2899 false, 83 void), max. score: 17746
Quantile-Plot 60003788469212692635-6152100846330206646551178836422893831876-99128224158142418705221196320486957511054110735
CPU time110000 s110000 s45000 s150000 s370000 s280000 s730000 s390000 s7500 s180000 s79000 s180000 s440 s230000 s200000 s60 s40000 s580000 s28000 s140000 s85000 s280000 s220000 s240000 s680000 s690000 s
ReachSafety-Arrays
433 valid tasks (320 true, 113 false, 0 void), max. score: 753
Quantile-Plot 0179214122-522852417676-1925926115052680-47061012612521821908392722695
CPU time1100 s560 s1900 s200 s2400 s14000 s3900 s9300 s2000 s120 s2900 s910 s3300 s0 s13 s2500 s0 s3.9 s5.2 s1400 s2100 s2600 s1000 s2200 s3100 s5500 s14000 s18000 s
ReachSafety-BitVectors
49 valid tasks (34 true, 15 false, 0 void), max. score: 83
Quantile-Plot 4549493425492867764442235505732225537-65412724049335540507171
CPU time240 s690 s1100 s120 s6.3 s1800 s3900 s4400 s8500 s57 s780 s770 s530 s0 s210 s1900 s1.3 s1700 s950 s0.30 s8.7 s3100 s73 s1100 s980 s2200 s1700 s3800 s3500 s2400 s
ReachSafety-ControlFlow
66 valid tasks (37 true, 29 false, 0 void), max. score: 103
Quantile-Plot 30-21520-242-241-4824432-223213-32-16726-89-207-672328-317-18736164143434346
CPU time8.1 s1900 s1500 s40 s720 s1300 s3200 s65 s9.2 s240 s2800 s35 s150 s1.6 s1300 s910 s0 s260 s27 s880 s5.3 s2900 s500 s1200 s1700 s880 s1300 s1100 s
ReachSafety-ECA
1263 valid tasks (783 true, 480 false, 0 void), max. score: 2046
Quantile-Plot 54127877308155245101011441014721067036906521-12432299026127342395637037112121252
CPU time73000 s4600 s370 s75000 s39000 s21000 s160000 s130000 s320 s55000 s25 s70000 s0 s26000 s0 s59000 s36 s28 s4.5 s64000 s6900 s5900 s32000 s82000 s55000 s21000 s240000 s180000 s
ReachSafety-Floats
1072 valid tasks (804 true, 268 false, 8 void), max. score: 1876
Quantile-Plot 642858723529-254-480-3968757313608260-4885333742-312539112790-7069373555416619733841
CPU time3500 s1900 s3200 s310 s24000 s43000 s11000 s9100 s25000 s210 s10000 s1500 s14000 s340 s2.4 s11000 s11000 s180 s11000 s3200 s2100 s2700 s42000 s36000 s38000 s19000 s18000 s
ReachSafety-Heap
239 valid tasks (166 true, 73 false, 1 void), max. score: 405
Quantile-Plot 21829228628924318927911242224290130280133-23481903082293123084245229190310300
CPU time1200 s330 s650 s100 s9800 s730 s4000 s600 s110 s930 s5.6 s840 s24 s3500 s3800 s4.8 s130 s3400 s13 s210 s420 s14 s7400 s7500 s6400 s13000 s6600 s
ReachSafety-Loops
729 valid tasks (528 true, 201 false, 61 void), max. score: 1257
Quantile-Plot 4628478777824025352597935284807254277170639236549161-7810673298708680888276847602843960921
CPU time8800 s9400 s35000 s9300 s5200 s28000 s28000 s27000 s58000 s460 s20000 s4500 s13000 s0 s8300 s52 s13000 s7400 s8.9 s14000 s820 s12000 s4800 s40000 s9500 s35000 s34000 s40000 s50000 s35000 s
ReachSafety-ProductLines
597 valid tasks (332 true, 265 false, 0 void), max. score: 929
Quantile-Plot 7064532252553522529270223805060508673808076896409111315170566317572900910
CPU time1900 s2200 s490 s390 s21000 s27000 s81000 s0 s3100 s20000 s0 s600 s0 s23000 s93 s9200 s18000 s31000 s17000 s21 s17000 s0 s13000 s7500 s22000 s98000 s76000 s
ReachSafety-Recursive
156 valid tasks (102 true, 54 false, 6 void), max. score: 258
Quantile-Plot 0118145124103-19611172711300127010880-334-252-144412412136121150591639415110497
CPU time0 s2200 s860 s270 s4500 s1500 s930 s450 s79 s1100 s0 s2300 s0 s550 s140 s1200 s62 s1.5 s780 s6.2 s1600 s190 s2800 s4200 s10000 s2800 s8300 s2900 s5500 s
ReachSafety-Sequentialized
584 valid tasks (184 true, 400 false, 0 void), max. score: 768
Quantile-Plot 152815880401316522165-77-25115643872-27524450234333543941-104476533
CPU time2900 s9400 s550 s3200 s91000 s62000 s69000 s9300 s850 s21000 s640 s850 s1.0 s16000 s30 s0 s2.2 s52000 s2800 s11000 s9700 s12000 s11000 s5500 s65000 s76000 s
ReachSafety-XCSP
119 valid tasks (60 true, 59 false, 0 void), max. score: 179
Quantile-Plot 14814071165150015314798921601480152148-92896014614713546153744156155
CPU time2100 s7600 s12000 s2000 s7600 s0 s4600 s680 s210 s2200 s1000 s2400 s360 s0 s4400 s4800 s0 s790 s0 s5300 s2100 s5800 s5200 s2900 s7900 s10000 s7800 s4600 s
ReachSafety-Combinations
671 valid tasks (241 true, 430 false, 0 void), max. score: 912
Quantile-Plot 5520162230359137309266234402970130236003551192193810331110139224
CPU time1400 s8700 s400 s33000 s88000 s44000 s76000 s42000 s960 s13000 s0 s23000 s0 s44 s0 s51000 s0 s0 s37000 s3200 s16000 s5700 s15000 s1200 s19000 s37000 s50000 s
ReachSafety-Hardware
1224 valid tasks (727 true, 497 false, 0 void), max. score: 1951
Quantile-Plot 9220110158-476-19269247-910814418805017992-76166012820123149152180156211166
CPU time2700 s36000 s17000 s170 s110 s8800 s59000 s21000 s360 s1800 s5200 s590 s0 s110 s20000 s11000 s0 s41 s13000 s3.7 s18000 s3400 s15000 s15000 s20000 s37000 s44000 s
ReachSafety-Hardness
4005 valid tasks (4005 true, 0 false, 7 void), max. score: 8010
Quantile-Plot 5870-40818262548148059085202-42264874657746813463070-61324432454046821223044848645856886014
CPU time15000 s37 s18 s43 s24000 s72000 s210000 s99000 s660 s29000 s62000 s48000 s8.9 s28000 s140000 s5.4 s7500 s350000 s2800 s13000 s9700 s36000 s40000 s34000 s93000 s170000 s
ReachSafety-Fuzzle
15 valid tasks (0 true, 15 false, 0 void), max. score: 15
Quantile-Plot 0111101140000150159001411089800
CPU time0 s29 s710 s6.0 s2300 s94 s3900 s0 s0 s0 s0 s470 s0 s3100 s2500 s0 s0 s4700 s8.1 s20 s0 s740 s930 s810 s0 s0 s
MemSafety
2080 valid tasks (1850 true, 230 false, 55 void), max. score: 3216
Quantile-Plot 224189013121330165520391897298207713041627151623212902156211014002014
CPU time1600 s820 s1500 s2600 s20000 s14000 s21000 s290 s7500 s240 s57000 s4200 s4400 s200 s2800 s220000 s87000 s130000 s
MemSafety-Arrays
222 valid tasks (185 true, 37 false, 0 void), max. score: 407
Quantile-Plot 125352-243322271234114231051722310529152333148265
CPU time23 s52 s110 s310 s810 s190 s140 s12 s32 s12 s870 s1400 s2000 s600 s100 s9.6 s110 s11000 s9700 s11000 s
MemSafety-Heap
188 valid tasks (94 true, 94 false, 0 void), max. score: 282
Quantile-Plot 202041359781197100-5819636178149401822187314410790103
CPU time130 s230 s310 s690 s4100 s1600 s2800 s150 s1900 s2.1 s1100 s3100 s460 s1500 s2400 s58 s400 s7200 s7100 s6100 s
MemSafety-LinkedLists
103 valid tasks (75 true, 28 false, 31 void), max. score: 178
Quantile-Plot 8412411912712312712684128211437581141601713018912
CPU time1300 s41 s71 s300 s1500 s730 s860 s64 s480 s0.11 s770 s1400 s45 s890 s100 s130 s200 s1700 s1700 s3000 s
MemSafety-Other
112 valid tasks (80 true, 32 false, 0 void), max. score: 192
Quantile-Plot 27118-18601171351365215611668761427213419119174113170
CPU time9.6 s64 s81 s39 s4400 s1600 s1000 s63 s180 s10 s430 s1600 s89 s1500 s820 s5.7 s740 s4500 s6300 s3700 s
MemSafety-Juliet
1414 valid tasks (1414 true, 0 false, 0 void), max. score: 2828
Quantile-Plot 02752275228282828267628280282826982828280422242828275202752250618342766
CPU time0 s430 s920 s1300 s8700 s9900 s16000 s0 s4900 s220 s12000 s49000 s1700 s14000 s860 s0 s1300 s200000 s60000 s110000 s
MemSafety-MemCleanup
41 valid tasks (2 true, 39 false, 24 void), max. score: 43
Quantile-Plot -2644-1073534019002403536041262723
CPU time180 s0.35 s1.1 s1.3 s67 s230 s260 s0 s13 s0 s0 s770 s0 s300 s92 s0 s47 s1400 s2300 s1000 s
ConcurrencySafety
3129 valid tasks (2550 true, 579 false, 130 void), max. score: 5672
Quantile-Plot 0117122941911-49242029-124783547 *)3906365421853258353-8289-1502477252123823543079318902655
CPU time0 s4.4 s1.7 s10000 s1600 s70000 s2100 s73000 s52000 s51000 s34000 s250000 s49000 s76000 s2100 s2900 s960 s22000 s41000 s23000 s250 s27000 s100000 s120000 s0 s84000 s
ConcurrencySafety-Main
685 valid tasks (348 true, 337 false, 27 void), max. score: 1033
Quantile-Plot 0224538213-1707454586581883341389-1302139039872-5178504116462481-203825456180512
CPU time0 s0.23 s0.56 s6000 s290 s22000 s340 s29000 s12000 s11000 s1000 s34000 s160000 s4500 s10000 s59 s30000 s2800 s5.5 s5900 s3700 s9600 s23000 s28 s9800 s28000 s20000 s0 s22000 s
ConcurrencySafety-MemSafety
738 valid tasks (724 true, 14 false, 29 void), max. score: 1462
Quantile-Plot 0222432400-4544921128400356819952-32-32631-4584328-32-1506443393510345
CPU time0 s0.23 s0.56 s2.9 s110 s23000 s0 s0 s11000 s13000 s1200 s0 s0 s21000 s2200 s740 s0 s0 s530 s3900 s16000 s0 s6.9 s0 s4100 s8600 s8100 s0 s7900 s
ConcurrencySafety-NoOverflows
733 valid tasks (726 true, 7 false, 34 void), max. score: 1459
Quantile-Plot 0626672630401002-444895013060029458937044892-448827410022466581049107701073
CPU time0 s4.0 s0.58 s4000 s1200 s25000 s0 s16000 s9900 s13000 s1100 s0 s0 s23000 s48000 s350 s32 s140 s210 s4000 s22000 s16000 s220 s4900 s21000 s28000 s0 s22000 s
NoDataRace-Main
973 valid tasks (752 true, 221 false, 40 void), max. score: 1725
Quantile-Plot 00554-44721112 *)1411338016268664122012000700
CPU time0 s0 s28000 s19000 s14000 s15000 s900 s0 s14 s1200 s8000 s42000 s60000 s0 s32000 s
NoOverflows
8113 valid tasks (4507 true, 3606 false, 75 void), max. score: 13044
Quantile-Plot 59766465-413745771-1781286034900827210987059-17650-73312806313377370949773639231
CPU time7300 s36000 s3700 s22000 s16000 s66000 s8900 s0 s48000 s3600 s870 s110000 s1400 s7600 s4200 s57000 s220000 s150000 s240000 s
NoOverflows-Main
1881 valid tasks (1429 true, 452 false, 75 void), max. score: 3310
Quantile-Plot 14451245-598591-951207523401332-64415121414852-11390192020756391666265318062581424
CPU time4500 s25000 s1100 s2100 s15000 s21000 s8900 s0 s7400 s290 s340 s21000 s25000 s270 s2800 s21000 s4200 s9700 s78000 s61000 s91000 s5600 s
NoOverflows-Juliet
6232 valid tasks (3078 true, 3154 false, 0 void), max. score: 9310
Quantile-Plot 44935874-610766902-240846485008348372459280-29582-753086156554205911600454545828
CPU time2900 s12000 s2500 s20000 s700 s45000 s0 s0 s41000 s3300 s530 s0 s84000 s1200 s4900 s41000 s0 s48000 s140000 s87000 s150000 s
Termination
2298 valid tasks (1480 true, 818 false, 56 void), max. score: 4000
Quantile-Plot 1584148166111251289119501048890125685535261258324800
CPU time15000 s24000 s570 s17000 s23000 s99000 s0 s3800 s18000 s26000 s2200 s69000 s17000 s64000 s0 s0 s
Termination-BitVectors
36 valid tasks (22 true, 14 false, 1 void), max. score: 58
Quantile-Plot 3436142427150242-1162752453275200
CPU time4.7 s100 s21 s3.8 s87 s360 s0 s8.2 s0.16 s67 s460 s20 s3.2 s2700 s28 s730 s0 s0 s
Termination-MainControlFlow
294 valid tasks (220 true, 74 false, 0 void), max. score: 514
Quantile-Plot 272115386858223066126172271245564388940900
CPU time120 s1300 s19 s720 s3000 s38000 s0 s1200 s11 s3400 s5000 s2600 s79 s21000 s580 s6100 s0 s0 s
Termination-MainHeap
202 valid tasks (189 true, 13 false, 0 void), max. score: 391
Quantile-Plot 0481624260022960-100243522433600
CPU time0 s97 s8.7 s15 s79 s0 s0 s8.3 s7.1 s0 s82 s0 s1.9 s18000 s9.4 s7500 s0 s0 s
Termination-Other
1766 valid tasks (1049 true, 717 false, 55 void), max. score: 2815
Quantile-Plot 154416659761662206615790145410101431969123090224161796192800
CPU time15000 s22000 s520 s16000 s20000 s61000 s0 s2500 s18000 s55000 s20000 s41000 s2200 s27000 s17000 s50000 s0 s0 s
SoftwareSystems
3458 valid tasks (2762 true, 696 false, 355 void), max. score: 5251
Quantile-Plot 10-1082872-2569-1297-2439-280478476-1063536-322-2037-249172197-76687261233351
CPU time72 s84000 s1500 s5800 s64000 s96000 s99000 s150000 s9600 s24000 s19000 s87000 s57000 s1400 s53000 s150000 s16000 s140000 s99000 s180000 s
SoftwareSystems-AWS-C-Common-ReachSafety
197 valid tasks (101 true, 96 false, 144 void), max. score: 298
Quantile-Plot -36461874-41-232328970-255-2011142114923651137-135-96-79
CPU time10 s340 s220 s140 s1900 s600 s400 s250 s2700 s0 s81 s480 s640 s6.9 s3100 s2400 s29 s1700 s1200 s3600 s1000 s4200 s
SoftwareSystems-coreutils-MemSafety
140 valid tasks (30 true, 110 false, 0 void), max. score: 170
0-1600-144-4480-28800-1440-288-288-4640-320-16-128000
CPU time0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s
SoftwareSystems-coreutils-NoOverflows
30 valid tasks (30 true, 0 false, 0 void), max. score: 60
Quantile-Plot 0-1600-112-48000000000-96-48040-16000
CPU time0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s240 s0 s0 s0 s0 s0 s
SoftwareSystems-BusyBox-NoOverflows
54 valid tasks (21 true, 33 false, 13 void), max. score: 75
Quantile-Plot 02000000-32000000-320800444
CPU time0 s15 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s1100 s0 s0 s120 s190 s260 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety
2442 valid tasks (2211 true, 231 false, 20 void), max. score: 4653
Quantile-Plot 30663085-51704067133340332531056-22571732216325283038818347628781426281223163106
CPU time61 s83000 s120 s220 s62000 s56000 s96000 s98000 s150000 s470 s85 s9100 s23000 s19000 s83000 s52000 s49000 s150000 s6000 s140000 s98000 s170000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety
8 valid tasks (8 true, 0 false, 0 void), max. score: 16
Quantile-Plot 0000002200-96000001400000
CPU time0 s0 s0 s0 s0 s0 s390 s400 s0 s0 s0 s0 s0 s0 s0 s0 s150 s0 s0 s0 s0 s0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety
141 valid tasks (4 true, 137 false, 0 void), max. score: 145
Quantile-Plot 267711029048240138118832161222
CPU time0.59 s260 s780 s120 s820 s0 s650 s1400 s0 s130 s1.8 s710 s610 s6.0 s480 s0.43 s7800 s120 s88 s120 s
SoftwareSystems-Other-ReachSafety
22 valid tasks (21 true, 1 false, 9 void), max. score: 43
Quantile-Plot 011-32-32-31-288-2880000-1128-32-64-2721001000
CPU time0 s0.74 s1.8 s0 s0 s14 s0 s0 s0 s0 s0 s0 s0 s91 s0 s0 s0 s1200 s0 s2.9 s0 s0 s0 s
SoftwareSystems-Other-MemSafety
34 valid tasks (18 true, 16 false, 13 void), max. score: 52
Quantile-Plot 0-5-6-46-90000000-15-2931208-4000
CPU time0 s52 s56 s64 s170 s0 s0 s0 s0 s0 s0 s0 s44 s40 s440 s0 s4.4 s110 s0 s0 s0 s
SoftwareSystems-uthash-ReachSafety
138 valid tasks (138 true, 0 false, 54 void), max. score: 276
Quantile-Plot 02282280022800006000000-20801920228000
CPU time0 s55 s94 s0 s0 s890 s0 s0 s0 s0 s9.9 s0 s0 s0 s0 s0 s0 s560 s0 s97 s0 s0 s0 s
SoftwareSystems-uthash-MemSafety
138 valid tasks (66 true, 72 false, 54 void), max. score: 204
Quantile-Plot 0204204961740961440009696-2108969672204000
CPU time0 s110 s220 s5300 s5000 s0 s580 s1700 s0 s0 s0 s730 s2100 s200 s280 s700 s23 s1200 s0 s0 s0 s
SoftwareSystems-uthash-NoOverflows
114 valid tasks (114 true, 0 false, 48 void), max. score: 228
Quantile-Plot 0000000000003600-46420400000
CPU time0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s32 s0 s0 s0 s510 s0 s0 s0 s0 s0 s
FalsificationOverall
28002 valid tasks (19992 true, 8010 false, 698 void), max. score: 8817
Quantile-Plot 1311-6171959-3764-911848122562394-1538-902432474050313922913157
CPU time34000 s66000 s26000 s150000 s140000 s330000 s140000 s92000 s190000 s77000 s170000 s96000 s140000 s75000 s120000 s
Overall
30300 valid tasks (21472 true, 8828 false, 754 void), max. score: 49097
Quantile-Plot 1056412206-181778391-754521568357617896154585470-67311731517192263961059318042
CPU time140000 s260000 s52000 s200000 s480000 s1100000 s220000 s340000 s41000 s440000 s460000 s910000 s230000 s1000000 s560000 s860000 s
JavaOverall
587 valid tasks (241 true, 346 false, 0 void), max. score: 828
Quantile-Plot -2752616398325618382676182566
CPU time1200 s9200 s14000 s18000 s1600 s2000 s3400 s1500 s5700 s
ReachSafety-Java
587 valid tasks (241 true, 346 false, 0 void), max. score: 828
Quantile-Plot -2752616398325618382676182566
CPU time1200 s9200 s14000 s18000 s1600 s2000 s3400 s1500 s5700 s
ParticipantsPlots2LSaiseBRICKBubaakBubaak-SpLitCBMCCoVeriTeam-Verifier-AlgoSelectionCoVeriTeam-Verifier-ParallelPortfolioCPA-BAM-BnBCPA-BAM-SMGCPALockatorCPAcheckerCPVCruxCSeqDartagnanDeagleDIVINEEBFEmergenThetaESBMC-incrESBMC-kindFrama-C-SVGazer-ThetaGDart-LLVMGoblintGraves-CPAGraves-ParInferKornLazy-CSeqLF-checkerLocksmithMopsaPeSCo-CPAPICheckerPinakaPredatorHPPROTONsv-sanitizersSymbioticThetaUAutomizerUGemCutterUKojakUTaipanVeriAbsVeriAbsLVeriOoverCOASTALGDartJava-RangerJayHornJBMCJDartMLBSPFSWAT

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