ETAPS Logo TACAS 2025
14th Competition on Software Verification (SV-COMP 2025)

Results of the Competition

This web page presents the results of SV-COMP 2025 - 14th 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. CPAchecker
2. ESBMC-kind
3. CPV
Quantile-Plot
MemSafety
1. CPAchecker
2. Symbiotic
3. UAutomizer
Quantile-Plot
ConcurrencySafety
1. Deagle
2. Dartagnan
3. UGemCutter
Quantile-Plot
NoOverflows
1. UAutomizer
2. UTaipan
3. UKojak
Quantile-Plot
Termination
1. PROTON
2. UAutomizer
3. AProVE (KoAT + LoAT)
Quantile-Plot
SoftwareSystems
1. CPAchecker
2. Mopsa
3. Symbiotic
Quantile-Plot
FalsificationOverall
1. CPAchecker
2. Symbiotic
3. Bubaak
Quantile-Plot
Overall
1. UAutomizer
2. CPAchecker
3. Symbiotic
Quantile-Plot
JavaOverall
1. Java-Ranger
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 '–' 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.

ParticipantsPlots2LSaiseAProVE (KoAT + LoAT)BRICKBubaakBubaak-SpLitCBMCCoOpeRaceCPA-BAM-BnBCPA-BAM-SMGCPALockatorCPAcheckerCPVCruxCSeqDartagnanDeagleDIVINEEBFEmergenThetaESBMC-incrESBMC-kindFrama-C-SVGazer-ThetaGDart-LLVMGoblintGraves-CPAHornixInferKornLazy-CSeqLF-checkerLocksmithMopsaNacpaPeSCo-CPAPICheckerPinakaPredatorHPPROTONRacerFsv-sanitizersSVF-SVCSymbioticThetaThornUAutomizerUGemCutterUKojakUTaipanVeriAbsVeriAbsLVeriOoverCOASTALGDartJava-RangerJayHornJBMCJDartMLBSPFSWAT
Representing Jury MemberViktor MalíkZhenbang ChenNils LommenLei BuMarek ChalupaMarek ChalupaHors ConcoursVesal VojdaniHors ConcoursHors ConcoursHors ConcoursMarian Lingsch-RosenfeldPo-Chun ChienHors ConcoursHors ConcoursHernán Ponce de LeónFei HeHors ConcoursHors ConcoursLevente BajcziTong WuTong WuHors ConcoursHors ConcoursHors ConcoursSimmo SaanHors ConcoursMartin BlichaHors ConcoursGidon ErnstHors ConcoursHors ConcoursHors ConcoursRaphaël MonatHenrik WachowitzHors ConcoursHors ConcoursHors ConcoursHors ConcoursRavindra MettaTomáš DacíkSimmo SaanMatthew RichardsMartin JonášLevente BajcziLevente BajcziMatthias HeizmannDominik KlumppManuel BenteleDaniel DietschPriyanka DarkePriyanka DarkeHors ConcoursHors ConcoursFalk HowarSoha HusseinHors ConcoursPeter SchrammelHors ConcoursLei BuHors ConcoursNils Loose
AffiliationBrno University of Technology, CzechiaNational University of Defense Technology, ChinaRWTH Aachen, GermanyNanjing University, ChinaISTA, AustriaISTA, Austria--, --University of Tartu, Estonia--, ----, ----, --LMU Munich, GermanyLMU Munich, Germany--, ----, --Huawei Dresden Research Center, GermanyTsinghua University, China--, ----, --Budapest University of Technology and Economics, Hungarythe University of Manchester, UKUniversity of Manchester, UK--, ----, ----, --University of Tartu, Estonia--, --University of Lugano, Switzerland--, --LMU Munich, Germany--, ----, ----, --Inria and University of Lille, FranceLMU Munich, Germany--, ----, ----, ----, --TCS, IndiaBrno University of Technology, Czech RepublicUniversity of Tartu, EstoniaUniversity of New South Wales, AustraliaMasaryk University, Brno, CzechiaBudapest University of Technology and Economics, HungaryBudapest 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, GermanyAin Shams University, Egypt--, --Diffblue Ltd., UK--, --Nanjing University, China--, --University of Luebeck, Germany
ReachSafety
11268 valid tasks (8347 true, 2921 false, 35 void), max. score: 17860
Quantile-Plot 6053668460531330103687755213346292106871724274041-9648928071027062692448-6871770973277-25195666493560071101211224
CPU time110000 s140000 s160000 s130000 s530000 s570000 s7400 s170000 s190000 s250000 s670 s230000 s2500 s33000 s330000 s680000 s26000 s21000 s130000 s110000 s57000 s290000 s230000 s250000 s690000 s670000 s
ReachSafety-Arrays
433 valid tasks (320 true, 113 false, 0 void), max. score: 753
Quantile-Plot 2182215205-527677-19257211705469-45581591276123127-2572222722988495721692
CPU time1600 s480 s5500 s14000 s2000 s1600 s1800 s100 s2900 s3.2 s3800 s0 s8.0 s2000 s26 s980 s230 s850 s1100 s1600 s72 s2700 s2900 s3.3 s3100 s3100 s5000 s13000 s15000 s
ReachSafety-BitVectors
49 valid tasks (34 true, 15 false, 0 void), max. score: 83
Quantile-Plot 4548494935737647422155059322459-64416717240-3894929242842547171
CPU time200 s600 s1000 s680 s12 s2200 s7600 s76 s760 s2800 s450 s0 s360 s1600 s1.6 s1400 s2.7 s39 s1200 s2800 s56 s12 s1000 s1100 s630 s2900 s1400 s3400 s3100 s2000 s
ReachSafety-ControlFlow
66 valid tasks (37 true, 29 false, 0 void), max. score: 103
Quantile-Plot 302319-2424832-213224-34-16528-89-664341248-304-187-4293718-3424043444447
CPU time5.5 s2300 s1200 s37 s400 s87 s7.2 s240 s1600 s20 s140 s1.8 s1100 s8.0 s300 s280 s170 s900 s5.0 s3.9 s3300 s540 s400 s850 s2100 s1700 s1300 s950 s
ReachSafety-ECA
1263 valid tasks (783 true, 480 false, 0 void), max. score: 2046
Quantile-Plot 565315270308102711491014931127037212840-119672210351250261-2008274372468106437942114001454
CPU time71000 s26000 s29000 s67000 s120000 s110000 s320 s53000 s580 s84000 s0 s25000 s24 s70000 s440 s13 s4.1 s80000 s100000 s4800 s7100 s6000 s32000 s22000 s91000 s53000 s31000 s240000 s180000 s
ReachSafety-Floats
1087 valid tasks (807 true, 280 false, 8 void), max. score: 1894
Quantile-Plot 644871695662-281765306610258-766133942-351118765793-103-198269955-14660526654737842
CPU time3600 s2000 s1800 s3300 s22000 s7800 s25000 s170 s8100 s4600 s15000 s300 s2.4 s9800 s320 s6200 s9600 s2600 s110 s2400 s3900 s7.8 s50000 s45000 s39000 s17000 s14000 s
ReachSafety-Heap
240 valid tasks (167 true, 73 false, 0 void), max. score: 407
Quantile-Plot 221276275291287112621011290134283-2270226287309229314-40031070-20245225226310300
CPU time1000 s350 s430 s93 s2600 s580 s96 s940 s270 s290 s15 s3000 s19 s490 s810 s3200 s12 s170 s6.1 s330 s400 s50 s7500 s6300 s6700 s11000 s5200 s
ReachSafety-Loops
774 valid tasks (565 true, 209 false, 0 void), max. score: 1339
Quantile-Plot 47810318718793798055254937275597270636246560296-8076871376759710687-5423860439476885639856961922
CPU time8000 s26000 s34000 s20000 s4200 s17000 s53000 s480 s20000 s35000 s11000 s0 s8300 s150 s10000 s680 s43 s28000 s2100 s7200 s12000 s5700 s78 s33000 s19000 s21000 s26000 s33000 s34000 s50000 s32000 s
ReachSafety-ProductLines
597 valid tasks (332 true, 265 false, 0 void), max. score: 929
Quantile-Plot 70628522725592790822380407830869416811650927911131051700575365567902911
CPU time1600 s13000 s800 s350 s22000 s87000 s3000 s18000 s0 s580 s0 s22000 s110 s7700 s20000 s8500 s17000 s18 s0 s16000 s0 s0 s13000 s8100 s31000 s93000 s66000 s
ReachSafety-Recursive
158 valid tasks (105 true, 53 false, 2 void), max. score: 263
Quantile-Plot 08711611511374711290127010682-329138-147414660113136122-16161498801269615010798
CPU time0 s2800 s1700 s200 s800 s550 s62 s870 s0 s2800 s0 s720 s46 s1000 s320 s13 s1400 s1100 s240 s1400 s150 s10 s2800 s6400 s0 s8200 s2600 s7500 s4300 s5300 s
ReachSafety-Sequentialized
585 valid tasks (185 true, 400 false, 0 void), max. score: 770
Quantile-Plot 1126627079551169-102-2121624398-2483354539465234-94823408430454532481541
CPU time1900 s8900 s28000 s2700 s46000 s8500 s870 s21000 s120 s730 s1.2 s16000 s150 s540 s3.7 s30000 s53000 s2300 s120 s11000 s15000 s5500 s16000 s12000 s9600 s61000 s71000 s
ReachSafety-XCSP
119 valid tasks (60 true, 59 false, 0 void), max. score: 179
Quantile-Plot 14814214015915314610091141581500152-8701320150147147-71714013640123639155154
CPU time1400 s8100 s18000 s790 s3500 s530 s180 s2200 s8700 s1900 s440 s0 s3500 s100 s2300 s0 s2500 s5300 s1600 s670 s6000 s4500 s4400 s1400 s6300 s6400 s6300 s3300 s
ReachSafety-Combinations
671 valid tasks (241 true, 430 false, 0 void), max. score: 912
Quantile-Plot 651851602333162812347030401302430292389119-4452222341210129112187289
CPU time1500 s8400 s14000 s30000 s87000 s55000 s910 s14000 s0 s19000 s0 s41 s0 s47000 s0 s52000 s44000 s2500 s13 s15000 s5500 s1700 s16000 s910 s17000 s42000 s63000 s
ReachSafety-Hardware
1224 valid tasks (727 true, 497 false, 0 void), max. score: 1951
Quantile-Plot 10014613758276248-99896198054190-7565702566420-31541131660134152127207171
CPU time1800 s16000 s9600 s130 s50000 s15000 s340 s1600 s20000 s610 s0 s310 s23000 s940 s640 s26000 s16000 s3.2 s120 s14000 s4000 s0 s13000 s8400 s11000 s32000 s43000 s
ReachSafety-Hardness
3987 valid tasks (3984 true, 3 false, 25 void), max. score: 7971
Quantile-Plot 589429938927061046566-416660809695241469-6014651860845150564742621739216050287882469027230
CPU time13000 s8400 s22000 s52 s170000 s210000 s720 s31000 s110000 s110000 s0.49 s30000 s4.3 s7300 s110000 s410000 s4300 s13000 s13000 s17000 s1800 s42000 s44000 s44000 s110000 s170000 s
ReachSafety-Fuzzle
15 valid tasks (0 true, 15 false, 0 void), max. score: 15
Quantile-Plot 01111400001501512-128015141-28810035411
CPU time0 s24 s66 s5.3 s3500 s0 s0 s0 s0 s470 s0 s2800 s270 s0 s0 s2700 s4400 s6.3 s0 s26 s0 s0 s210 s430 s340 s76 s94 s
MemSafety
4042 valid tasks (1958 true, 2084 false, 0 void), max. score: 6409
Quantile-Plot 6863355334918853249488250231582198269748774733861-109654479600390929393711
CPU time1500 s2500 s5000 s3600 s28000 s66000 s290 s9000 s240 s33000 s33000 s5600 s1900 s32 s8100 s1500 s130000 s100000 s130000 s
MemSafety-Arrays
220 valid tasks (184 true, 36 false, 0 void), max. score: 404
Quantile-Plot 05353-24231281235104221241242210128-296167-9346149275
CPU time0 s46 s100 s290 s230 s590 s12 s24 s8.1 s820 s1400 s54 s560 s97 s7.1 s1.3 s81 s71 s12000 s9900 s10000 s
MemSafety-Heap
247 valid tasks (138 true, 109 false, 0 void), max. score: 385
Quantile-Plot 102287287187297329-2230911621815432922233190-582325-78165150199
CPU time120 s450 s680 s590 s2000 s4500 s200 s2100 s7.0 s1200 s300 s2900 s1600 s2500 s23 s6.3 s1100 s390 s7300 s11000 s8200 s
MemSafety-LinkedLists
134 valid tasks (106 true, 28 false, 0 void), max. score: 240
Quantile-Plot 9011411412712720884962114962081142201701300221014
CPU time1100 s71 s170 s250 s790 s2000 s61 s430 s0.11 s710 s120 s1000 s800 s110 s25 s0 s140 s0 s3400 s2300 s3800 s
MemSafety-Other
105 valid tasks (90 true, 15 false, 0 void), max. score: 195
Quantile-Plot 355049-2042144165115439136144411334-230128131171157171
CPU time28 s440 s320 s630 s1300 s660 s12 s140 s19 s1000 s84 s120 s1100 s580 s1.5 s4.7 s1600 s1100 s2200 s4000 s2400 s
MemSafety-Juliet
3271 valid tasks (1438 true, 1833 false, 0 void), max. score: 4709
Quantile-Plot 040904090385141244709045732746436025304645450545621779-2032845270322222683158
CPU time0 s1400 s3600 s1800 s24000 s58000 s0 s6300 s200 s25000 s31000 s29000 s30000 s2200 s1800 s18 s5200 s0 s100000 s70000 s100000 s
MemSafety-MemCleanup
65 valid tasks (2 true, 63 false, 0 void), max. score: 67
Quantile-Plot -2665651459630440026559605-271650515349
CPU time170 s54 s130 s5.6 s440 s480 s0 s19 s0 s0 s1.1 s61 s440 s84 s1.3 s2.3 s84 s0 s2400 s4100 s2500 s
ConcurrencySafety
3175 valid tasks (2542 true, 633 false, 4 void), max. score: 5733
Quantile-Plot 0-190-189818-49681770-1272033834604344356214921502448-8976-15153396014524596022722982993314402593
CPU time0 s4.6 s13 s9100 s2500 s51000 s40000 s61000 s11000 s30000 s200000 s120000 s120000 s820 s910 s18000 s41000 s0 s59000 s26000 s19 s41000 s1800 s87000 s180000 s0 s76000 s
ConcurrencySafety-Main
724 valid tasks (373 true, 351 false, 1 void), max. score: 1097
Quantile-Plot 0-96-96116-1744450512538843314343369367114311-53314598804343964451251505796610583
CPU time0 s0 s0 s5700 s490 s23000 s9300 s15000 s3200 s30000 s150000 s10000 s10000 s15 s28000 s84 s4500 s2500 s0 s18000 s7100 s26000 s2.4 s21000 s0 s21000 s44000 s0 s22000 s
ConcurrencySafety-MemSafety
751 valid tasks (716 true, 35 false, 1 void), max. score: 1467
Quantile-Plot 0-90-90000-4488852122800697697896-32393-451413600-32-1407163003400307
CPU time0 s0.56 s2.0 s0 s0 s0 s7700 s14000 s2600 s0 s0 s1200 s1100 s300 s0 s450 s3100 s15000 s0 s0 s0 s0.70 s0 s9200 s7700 s9700 s0 s7400 s
ConcurrencySafety-NoOverflows
672 valid tasks (660 true, 12 false, 1 void), max. score: 1332
Quantile-Plot 09105850792-43008341142005155172344476-4312132050177238402678719060871
CPU time0 s4.0 s11 s3400 s0 s9300 s7800 s12000 s2200 s0 s0 s41000 s42000 s92 s30 s160 s3400 s23000 s0 s25000 s13000 s4.6 s17 s2300 s18000 s30000 s0 s21000 s
NoDataRace-Main
1028 valid tasks (793 true, 235 false, 1 void), max. score: 1821
Quantile-Plot 001482442-447911751338518142419204981352108823131112820778
CPU time0 s0 s4000 s19000 s16000 s20000 s3100 s71000 s410 s16 s0 s16000 s990 s1200 s8900 s39000 s94000 s0 s26000 s
NoOverflows
8211 valid tasks (4552 true, 3659 false, 10 void), max. score: 13297
Quantile-Plot 688765726556720087776080-361866815738486-76213849188439581723-194697704-170-28611074887810736
CPU time10000 s52000 s43000 s26000 s62000 s9000 s0 s33000 s50000 s4100 s840 s1400 s9000 s15000 s3800 s1500 s130 s54000 s7700 s9300 s240000 s190000 s260000 s
NoOverflows-Main
1979 valid tasks (1474 true, 505 false, 10 void), max. score: 3453
Quantile-Plot 155313641363123621192930-1741528-63621841601-13091213821512263462541-93851811-82-138275619062631-366
CPU time8000 s33000 s26000 s7800 s21000 s9000 s0 s33000 s12000 s270 s360 s24000 s250 s4200 s12000 s23000 s3800 s200 s130 s13000 s7700 s9300 s73000 s61000 s82000 s5800 s
NoOverflows-Juliet
6232 valid tasks (3078 true, 3154 false, 0 void), max. score: 9310
Quantile-Plot 556356815660703766500008346439060040-7446461566650568109120599200813174748011
CPU time2300 s19000 s17000 s18000 s41000 s0 s0 s0 s38000 s3800 s480 s0 s1200 s4800 s3200 s38000 s0 s1300 s0 s41000 s0 s0 s170000 s130000 s180000 s
Termination
2328 valid tasks (1531 true, 797 false, 11 void), max. score: 4079
Quantile-Plot 170322191491112211991301062011159690129092236851411712536333400
CPU time13000 s120000 s13000 s14000 s14000 s54000 s0 s47000 s3300 s16000 s0 s37000 s1900 s87000 s17000 s24000 s4600 s64000 s0 s0 s
Termination-BitVectors
34 valid tasks (23 true, 11 false, 0 void), max. score: 57
Quantile-Plot 36833252617011264-11501772655331005200
CPU time5.1 s35 s65 s100 s3.9 s81 s0 s880 s7.4 s0.23 s62 s0 s3.2 s23 s2.6 s2800 s28 s140 s0 s610 s0 s0 s
Termination-MainControlFlow
272 valid tasks (215 true, 57 false, 9 void), max. score: 487
Quantile-Plot 27439714578682210283661261670222241564319133433240200
CPU time170 s2600 s880 s1100 s630 s2300 s0 s45000 s990 s9.3 s3100 s0 s750 s2400 s80 s26000 s440 s23000 s3700 s4900 s0 s0 s
Termination-MainHeap
202 valid tasks (189 true, 13 false, 0 void), max. score: 391
Quantile-Plot 02863624240002294000024352240033400
CPU time0 s4800 s52 s72 s12 s0 s0 s0 s7.6 s6.7 s0 s0 s0 s0 s1.6 s23000 s6.2 s0 s0 s5700 s0 s0 s
Termination-Other
1820 valid tasks (1104 true, 716 false, 2 void), max. score: 2924
Quantile-Plot 1565127916021433168816790-54414541126150501639124590225241821-544-544194400
CPU time13000 s110000 s12000 s13000 s13000 s52000 s0 s920 s2300 s16000 s58000 s0 s36000 s41000 s1900 s35000 s17000 s920 s930 s52000 s0 s0 s
SoftwareSystems
4329 valid tasks (3249 true, 1080 false, 179 void), max. score: 7131
Quantile-Plot 116971649-2586-2370-4079217872-1948545-670-3298720862127-159801822654300288
CPU time62 s95000 s22000 s8500 s90000 s91000 s110000 s9700 s22000 s68000 s84000 s1500 s73000 s81000 s150000 s0 s22000 s140000 s100000 s130000 s
SoftwareSystems-AWS-C-Common-ReachSafety
341 valid tasks (177 true, 164 false, 0 void), max. score: 518
Quantile-Plot -26326323982332180-465-1719160150761812102975431-46
CPU time12 s1700 s4300 s240 s650 s370 s6000 s190 s560 s1200 s8.1 s7000 s1300 s3500 s2200 s0 s2200 s18000 s1900 s12000 s
SoftwareSystems-coreutils-MemSafety
139 valid tasks (29 true, 110 false, 2 void), max. score: 168
000-1440-27200-800-272-46400-304000000
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
29 valid tasks (29 true, 0 false, 1 void), max. score: 58
Quantile-Plot 000-112003800-16000-4324380000000
CPU time0 s0 s0 s0 s0 s0 s670 s0 s0 s0 s0 s0 s0 s0 s67 s190 s0 s0 s0 s0 s0 s0 s0 s
SoftwareSystems-BusyBox-NoOverflows
66 valid tasks (34 true, 32 false, 1 void), max. score: 100
Quantile-Plot 0000004-480-16044-60684-12000000
CPU time0 s0 s0 s0 s0 s0 s1200 s0 s0 s0 s0 s7.7 s1200 s0.30 s450 s1200 s1200 s0 s0 s0 s0 s0 s0 s
SoftwareSystems-DeviceDriversLinux64-ReachSafety
2405 valid tasks (2185 true, 220 false, 15 void), max. score: 4590
Quantile-Plot 298583531-5178326932203062-2247272219482984296036023027278401384252421042531
CPU time50 s91000 s14000 s94 s89000 s88000 s87000 s110 s9200 s20000 s68000 s73000 s69000 s70000 s140000 s0 s8600 s110000 s98000 s120000 s
SoftwareSystems-DeviceDriversLinux64Large-ReachSafety
8 valid tasks (8 true, 0 false, 0 void), max. score: 16
Quantile-Plot 0000224-96000044000000
CPU time0 s0 s0 s0 s370 s340 s190 s0 s0 s0 s0 s0 s140 s270 s0 s0 s0 s0 s0 s0 s
SoftwareSystems-DeviceDriversLinux64-MemSafety
141 valid tasks (4 true, 137 false, 0 void), max. score: 145
Quantile-Plot 2929010054770789881381069212
CPU time0.53 s1700 s3000 s100 s0 s760 s3900 s0 s50 s2.2 s770 s5.7 s3500 s550 s0.41 s0 s9300 s110 s48 s110 s
SoftwareSystems-Intel-TDX-Module-ReachSafety
146 valid tasks (102 true, 44 false, 144 void), max. score: 248
Quantile-Plot 0000-120-1200-16320-6400-120-251200-8600000
CPU time0 s0 s0 s0 s160 s160 s0 s0 s0 s36 s0 s88 s0 s0 s0 s2200 s0 s0 s0 s0 s0 s
SoftwareSystems-Other-ReachSafety
30 valid tasks (25 true, 5 false, 1 void), max. score: 55
Quantile-Plot 033-32-272-27240-160-6210-64-2881240502222
CPU time0 s4.1 s21 s0 s0 s0 s890 s0 s0 s4.4 s520 s0 s0 s190 s550 s510 s0 s24 s26 s34 s90 s
SoftwareSystems-Other-MemSafety
49 valid tasks (31 true, 18 false, 0 void), max. score: 80
Quantile-Plot 0-9-9-780000-3200-46914009012000
CPU time0 s12 s26 s170 s0 s0 s0 s0 s0 s0 s0 s32 s440 s0 s0 s140 s0 s210 s0 s0 s0 s
SoftwareSystems-uthash-ReachSafety
192 valid tasks (192 true, 0 false, 0 void), max. score: 384
Quantile-Plot 023623000007802200-2960192000234000
CPU time0 s160 s200 s0 s0 s0 s0 s260 s0 s720 s0 s0 s0 s520 s0 s0 s0 s75 s0 s0 s0 s
SoftwareSystems-uthash-MemSafety
192 valid tasks (90 true, 102 false, 0 void), max. score: 282
Quantile-Plot 02462461320138156000132-2741108156138780246000
CPU time0 s380 s650 s3900 s0 s940 s2100 s0 s0 s0 s950 s230 s290 s550 s1000 s24 s0 s1300 s0 s0 s0 s
SoftwareSystems-uthash-NoOverflows
162 valid tasks (162 true, 0 false, 0 void), max. score: 324
Quantile-Plot 0000000000000-46430000000600
CPU time0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s0 s590 s0 s0 s0 s0 s0 s1800 s0 s0 s
SoftwareSystems-uthash-MemCleanup
162 valid tasks (90 true, 72 false, 0 void), max. score: 252
Quantile-Plot 02162161261740000096138-822480216000
CPU time0 s210 s360 s3900 s7100 s0 s0 s0 s0 s0 s260 s420 s340 s14 s0 s300 s0 s0 s0 s
SoftwareSystems-DeviceDriversLinux64-Termination
267 valid tasks (91 true, 176 false, 15 void), max. score: 358
Quantile-Plot -167248-28729050629037324006225100
CPU time0 s120 s54 s110 s320 s0 s21 s1.3 s900 s0 s890 s1100 s67 s0 s61 s8300 s0 s0 s
FalsificationOverall
31025 valid tasks (20648 true, 10377 false, 228 void), max. score: 10903
Quantile-Plot 193055585556-386970373423885-721703226916480493138804732
CPU time38000 s65000 s130000 s140000 s360000 s130000 s97000 s190000 s210000 s190000 s100000 s210000 s140000 s190000 s
Overall
33353 valid tasks (22179 true, 11174 false, 239 void), max. score: 55561
Quantile-Plot 12658177681649790982677236691843417266450813521261151632420691297101287220244
CPU time130000 s300000 s250000 s190000 s870000 s210000 s460000 s87000 s450000 s150000 s550000 s1000000 s230000 s960000 s620000 s850000 s
JavaOverall
674 valid tasks (253 true, 421 false, 0 void), max. score: 927
Quantile-Plot -3960627676248628-1256581184492
CPU time1100 s7700 s21000 s15000 s1200 s2900 s6100 s1400 s5000 s
ReachSafety-Java
674 valid tasks (253 true, 421 false, 0 void), max. score: 927
Quantile-Plot -3960627676248628-1256581184492
CPU time1100 s7700 s21000 s15000 s1200 s2900 s6100 s1400 s5000 s
RuntimeException-Java
673 valid tasks (654 true, 19 false, 0 void), max. score: 1327
Quantile-Plot 727Demo383Demo974Demo
CPU time6600 s20000 s2600 s
ParticipantsPlots2LSaiseAProVE (KoAT + LoAT)BRICKBubaakBubaak-SpLitCBMCCoOpeRaceCPA-BAM-BnBCPA-BAM-SMGCPALockatorCPAcheckerCPVCruxCSeqDartagnanDeagleDIVINEEBFEmergenThetaESBMC-incrESBMC-kindFrama-C-SVGazer-ThetaGDart-LLVMGoblintGraves-CPAHornixInferKornLazy-CSeqLF-checkerLocksmithMopsaNacpaPeSCo-CPAPICheckerPinakaPredatorHPPROTONRacerFsv-sanitizersSVF-SVCSymbioticThetaThornUAutomizerUGemCutterUKojakUTaipanVeriAbsVeriAbsLVeriOoverCOASTALGDartJava-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