TACAS
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, bronze for third and light green for demo categories.

Here some brief directions for reading the score-based quantile plots:

  • The right end of the graph displays the achieved score. The score is SV-COMP's definition of quality. You can read the ranking on the top from right to left.
  • The left end of the graph displays the amount of wrong results that a verifier produced. Left-most start means worst.
  • The length of the graph displays the amount of correct verification work. Long is good.
  • More about what you can learn from a score-based quantile plot and how to interpret it, is described in the SV-COMP 2015 report, on pages 12 and 13.

Ranking by Category (with Score-Based Quantile Plots)

ReachSafety 1. CPAchecker 2. ESBMC-kind 3. CPV
Quantile plot for ReachSafety
MemSafety 1. CPAchecker 2. Symbiotic 3. UAutomizer
Quantile plot for MemSafety
ConcurrencySafety 1. Deagle 2. Dartagnan 3. UGemCutter
Quantile plot for ConcurrencySafety
NoOverflows 1. UAutomizer 2. UTaipan 3. UKojak
Quantile plot for NoOverflows
Termination 1. PROTON 2. UAutomizer 3. AProVE (KoAT + LoAT)
Quantile plot for Termination
SoftwareSystems 1. CPAchecker 2. Mopsa 3. Symbiotic
Quantile plot for SoftwareSystems
FalsificationOverall 1. CPAchecker 2. Symbiotic 3. Bubaak
Quantile plot for FalsificationOverall
Overall 1. UAutomizer 2. CPAchecker 3. Symbiotic
Quantile plot for Overall
JavaOverall 1. Java-Ranger 2. JBMC 3. GDart
Quantile plot for JavaOverall
Page 1 / 3

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.

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.

Participants Plots 2LS aise AProVE (KoAT + LoAT) BRICK Bubaak Bubaak-SpLit CBMC COASTAL CoOpeRace CPA-BAM-BnB CPA-BAM-SMG CPALockator CPAchecker CPV Crux CSeq Dartagnan Deagle DIVINE EBF EmergenTheta ESBMC-incr ESBMC-kind Frama-C-SV Gazer-Theta GDart GDart-LLVM Goblint Graves-CPA Hornix Infer Java-Ranger JayHorn JBMC JDart Korn Lazy-CSeq LF-checker Locksmith MLB Mopsa Nacpa PeSCo-CPA PIChecker Pinaka PredatorHP PROTON RacerF SPF SV-sanitizers SVF-SVC SWAT Symbiotic Theta Thorn UAutomizer UGemCutter UKojak UTaipan VeriAbs VeriAbsL VeriOover
Representing Jury Member Viktor Malík Zhenbang Chen Nils Lommen Lei Bu Marek Chalupa Marek Chalupa inactive inactive Vesal Vojdani inactive inactive inactive Marian Lingsch-Rosenfeld Po-Chun Chien inactive inactive Hernán Ponce de León Fei He inactive inactive Levente Bajczi Tong Wu Tong Wu inactive inactive Falk Howar inactive Simmo Saan inactive Martin Blicha inactive Soha Hussein inactive Peter Schrammel inactive Gidon Ernst inactive inactive inactive Lei Bu Raphaël Monat Henrik Wachowitz inactive inactive inactive inactive Ravindra Metta Tomáš Dacík inactive Simmo Saan Matthew Richards Nils Loose Martin Jonáš Levente Bajczi Levente Bajczi Matthias Heizmann Dominik Klumpp Manuel Bentele Daniel Dietsch Priyanka Darke Priyanka Darke inactive
Affiliation Brno University of Technology, Czechia National University of Defense Technology, China RWTH Aachen, Germany Nanjing University, China ISTA, Austria ISTA, Austria --,-- --,-- University of Tartu, Estonia --,-- --,-- --,-- LMU Munich, Germany LMU Munich, Germany --,-- --,-- Huawei Dresden Research Center, Germany Tsinghua University, China --,-- --,-- Budapest University of Technology and Economics, Hungary University of Manchester, UK University of Manchester, UK --,-- --,-- TU Dortmund, Germany --,-- University of Tartu, Estonia --,-- Charles University, Czechia --,-- Ain Shams University, Egypt --,-- Diffblue Ltd, United Kingdom --,-- LMU Munich, Germany --,-- --,-- --,-- Nanjing University, China Inria and University of Lille, France LMU Munich, Germany --,-- --,-- --,-- --,-- Tata Consultancy Services, India Brno University of Technology, Czechia --,-- University of Tartu, Estonia University of New South Wales, Australia University of Luebeck, Germany Masaryk University, Brno, Czechia Budapest University of Technology and Economics, Hungary Budapest University of Technology and Economics, Hungary University of Stuttgart, Germany LIX - CNRS - École Polytechnique, France University of Freiburg, Germany University of Freiburg, Germany Tata Consultancy Services, India Tata Consultancy Services, India --,--