TACAS
15th Competition on Software Verification (SV-COMP 2026)

Results of the Competition

This web page presents the results of SV-COMP 2026 - 15th 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.

Contents

1. C Verification

2. C.Huawei-Concurrency-Challenges Verification (Demo)

3. Java Verification

4. SV-LIB Verification (Demo)

1. C Verification

Ranking by Category (with Score-Based Quantile Plots)

C.ReachSafety 1. CPAchecker 2. ESBMC-kind 3. Symbiotic
Quantile plot for C.ReachSafety
C.MemSafety 1. Symbiotic 2. CPAchecker 3. UAutomizer
Quantile plot for C.MemSafety
C.Concurrency 1. Deagle 2. Dartagnan 3. iekke
Quantile plot for C.Concurrency
C.NoOverflows 1. UParalizer 2. UAutomizer 3. UTaipan
Quantile plot for C.NoOverflows
C.Termination 1. PROTON 2. UAutomizer 3. AProVE (KoAT + LoAT)
Quantile plot for C.Termination
C.SoftwareSystems 1. Mopsa 2. Symbiotic 3. CPAchecker
Quantile plot for C.SoftwareSystems
C.FalseOverall 1. Symbiotic 2. CPAchecker 3. UAutomizer
Quantile plot for C.FalseOverall
C.TrueOverall 1. UAutomizer 2. Goblint 3. Goblint-Par
Quantile plot for C.TrueOverall
C.Overall 1. UAutomizer 2. CPAchecker 3. Symbiotic
Quantile plot for C.Overall
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 can be found in the literature [Proc. TACAS 2024, Fig. 7, page 317] and the categories are defined on the respective SV-COMP web page.

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 DASA Deagle DIVINE EBF EmergenTheta ESBMC-incr ESBMC-kind Frama-C-SV ReFuncTion Gazer-Theta GDart GDart-LLVM Goblint Goblitch Graves-CPA Hornix iekke Infer Java-Ranger JayHorn JBMC JDart JLiSA Korn Lazy-CSeq LF-checker Locksmith MLB Mopsa MuVal Nacpa OGChecker PeSCo-CPA PIChecker Pinaka PredatorHP PROTON PySvLib-CHC RacerF Re3ver SEAL SPF SV-sanitizers SVF-SVC SvLibChecker SWAT Symbiotic Theta Thorn UAutomizer UGemCutter UKojak UParalizer UTaipan VeriAbs VeriAbsL VeriOover
Representing Jury Member inactive Zhenbang Chen Nils Lommen Lei Bu inactive inactive inactive inactive Vesal Vojdani inactive inactive inactive Marek Jankola Po-Chun Chien inactive Omar Inverso Hernán Ponce de León Felix Maechtle Fei He inactive inactive Levente Bajczi Xianzhiyu Li Xianzhiyu Li inactive Naïm Moussaoui Remil inactive Malte Mues inactive Simmo Saan Karoliine Holter inactive Martin Blicha Paolo Di Biase inactive inactive Hassan Mousavi Peter Schrammel inactive Giacomo Zanatta Gidon Ernst inactive inactive inactive Lei Bu Raphaël Monat Hiroshi Unno Henrik Wachowitz Zuchao Yang inactive inactive inactive inactive Ravindra Metta Gidon Ernst Tomáš Dacík Adéla Štěpková Tomáš Dacík inactive Simmo Saan Matthew Richards Marian Lingsch-Rosenfeld Nils Loose Martin Jonáš Csanád Telbisz Levente Bajczi Matthias Heizmann Dominik Klumpp Manuel Bentele Max Barth Daniel Dietsch inactive inactive inactive
Affiliation --,-- National University of Defense Technology, China RWTH Aachen, Germany Nanjing University, China --,-- --,-- --,-- --,-- University of Tartu, Estonia --,-- --,-- --,-- LMU Munich, Germany LMU Munich, Germany --,-- Gran Sasso Science Institute, Italy Huawei Dresden Research Center, Germany University of Luebeck, Germany Tsinghua University, China --,-- --,-- Budapest University of Technology and Economics, Hungary University of Manchester, UK University of Manchester, UK --,-- Inria Paris and École Normale Supérieure, France --,-- TU Dortmund, Germany --,-- University of Tartu, Estonia University of Tartu, Estonia --,-- Charles University, Czechia Unimol, Italy --,-- --,-- University of Tehran, Tehran Institute for Advanced Studies, Iran Diffblue Ltd, United Kingdom --,-- Ca' Foscari University of Venice, Italy LMU Munich, Germany --,-- --,-- --,-- Nanjing University, China Inria and University of Lille, France Tohoku University, Japan LMU Munich, Germany Xidian University, China --,-- --,-- --,-- --,-- Tata Consultancy Services, India LMU Munich, Germany Brno University of Technology, Czechia Masaryk University, Brno, Czechia Brno University of Technology, Czechia --,-- University of Tartu, Estonia University of New South Wales, Australia LMU Munich, Germany 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 LMU Munich, Germany University of Freiburg, Germany --,-- --,-- --,--

2. C.Huawei-Concurrency-Challenges Verification (Demo)

Ranking by Category (with Score-Based Quantile Plots)

C.Huawei-Concurrency-Challenges 1. Dartagnan 2. Goblint 3. Goblint-Par
Quantile plot for C.Huawei-Concurrency-Challenges
Page 1 / 1

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 can be found in the literature [Proc. TACAS 2024, Fig. 7, page 317] and the categories are defined on the respective SV-COMP web page.

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 DASA Deagle DIVINE EBF EmergenTheta ESBMC-incr ESBMC-kind Frama-C-SV ReFuncTion Gazer-Theta GDart GDart-LLVM Goblint Goblitch Graves-CPA Hornix iekke Infer Java-Ranger JayHorn JBMC JDart JLiSA Korn Lazy-CSeq LF-checker Locksmith MLB Mopsa MuVal Nacpa OGChecker PeSCo-CPA PIChecker Pinaka PredatorHP PROTON PySvLib-CHC RacerF Re3ver SEAL SPF SV-sanitizers SVF-SVC SvLibChecker SWAT Symbiotic Theta Thorn UAutomizer UGemCutter UKojak UParalizer UTaipan VeriAbs VeriAbsL VeriOover
Representing Jury Member inactive Zhenbang Chen Nils Lommen Lei Bu inactive inactive inactive inactive Vesal Vojdani inactive inactive inactive Marek Jankola Po-Chun Chien inactive Omar Inverso Hernán Ponce de León Felix Maechtle Fei He inactive inactive Levente Bajczi Xianzhiyu Li Xianzhiyu Li inactive Naïm Moussaoui Remil inactive Malte Mues inactive Simmo Saan Karoliine Holter inactive Martin Blicha Paolo Di Biase inactive inactive Hassan Mousavi Peter Schrammel inactive Giacomo Zanatta Gidon Ernst inactive inactive inactive Lei Bu Raphaël Monat Hiroshi Unno Henrik Wachowitz Zuchao Yang inactive inactive inactive inactive Ravindra Metta Gidon Ernst Tomáš Dacík Adéla Štěpková Tomáš Dacík inactive Simmo Saan Matthew Richards Marian Lingsch-Rosenfeld Nils Loose Martin Jonáš Csanád Telbisz Levente Bajczi Matthias Heizmann Dominik Klumpp Manuel Bentele Max Barth Daniel Dietsch inactive inactive inactive
Affiliation --,-- National University of Defense Technology, China RWTH Aachen, Germany Nanjing University, China --,-- --,-- --,-- --,-- University of Tartu, Estonia --,-- --,-- --,-- LMU Munich, Germany LMU Munich, Germany --,-- Gran Sasso Science Institute, Italy Huawei Dresden Research Center, Germany University of Luebeck, Germany Tsinghua University, China --,-- --,-- Budapest University of Technology and Economics, Hungary University of Manchester, UK University of Manchester, UK --,-- Inria Paris and École Normale Supérieure, France --,-- TU Dortmund, Germany --,-- University of Tartu, Estonia University of Tartu, Estonia --,-- Charles University, Czechia Unimol, Italy --,-- --,-- University of Tehran, Tehran Institute for Advanced Studies, Iran Diffblue Ltd, United Kingdom --,-- Ca' Foscari University of Venice, Italy LMU Munich, Germany --,-- --,-- --,-- Nanjing University, China Inria and University of Lille, France Tohoku University, Japan LMU Munich, Germany Xidian University, China --,-- --,-- --,-- --,-- Tata Consultancy Services, India LMU Munich, Germany Brno University of Technology, Czechia Masaryk University, Brno, Czechia Brno University of Technology, Czechia --,-- University of Tartu, Estonia University of New South Wales, Australia LMU Munich, Germany 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 LMU Munich, Germany University of Freiburg, Germany --,-- --,-- --,--

3. Java Verification

Ranking by Category (with Score-Based Quantile Plots)

Java.Overall 1. JBMC 2. GDart 3. JLiSA
Quantile plot for Java.Overall
Page 1 / 1

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 can be found in the literature [Proc. TACAS 2024, Fig. 7, page 317] and the categories are defined on the respective SV-COMP web page.

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 DASA Deagle DIVINE EBF EmergenTheta ESBMC-incr ESBMC-kind Frama-C-SV ReFuncTion Gazer-Theta GDart GDart-LLVM Goblint Goblitch Graves-CPA Hornix iekke Infer Java-Ranger JayHorn JBMC JDart JLiSA Korn Lazy-CSeq LF-checker Locksmith MLB Mopsa MuVal Nacpa OGChecker PeSCo-CPA PIChecker Pinaka PredatorHP PROTON PySvLib-CHC RacerF Re3ver SEAL SPF SV-sanitizers SVF-SVC SvLibChecker SWAT Symbiotic Theta Thorn UAutomizer UGemCutter UKojak UParalizer UTaipan VeriAbs VeriAbsL VeriOover
Representing Jury Member inactive Zhenbang Chen Nils Lommen Lei Bu inactive inactive inactive inactive Vesal Vojdani inactive inactive inactive Marek Jankola Po-Chun Chien inactive Omar Inverso Hernán Ponce de León Felix Maechtle Fei He inactive inactive Levente Bajczi Xianzhiyu Li Xianzhiyu Li inactive Naïm Moussaoui Remil inactive Malte Mues inactive Simmo Saan Karoliine Holter inactive Martin Blicha Paolo Di Biase inactive inactive Hassan Mousavi Peter Schrammel inactive Giacomo Zanatta Gidon Ernst inactive inactive inactive Lei Bu Raphaël Monat Hiroshi Unno Henrik Wachowitz Zuchao Yang inactive inactive inactive inactive Ravindra Metta Gidon Ernst Tomáš Dacík Adéla Štěpková Tomáš Dacík inactive Simmo Saan Matthew Richards Marian Lingsch-Rosenfeld Nils Loose Martin Jonáš Csanád Telbisz Levente Bajczi Matthias Heizmann Dominik Klumpp Manuel Bentele Max Barth Daniel Dietsch inactive inactive inactive
Affiliation --,-- National University of Defense Technology, China RWTH Aachen, Germany Nanjing University, China --,-- --,-- --,-- --,-- University of Tartu, Estonia --,-- --,-- --,-- LMU Munich, Germany LMU Munich, Germany --,-- Gran Sasso Science Institute, Italy Huawei Dresden Research Center, Germany University of Luebeck, Germany Tsinghua University, China --,-- --,-- Budapest University of Technology and Economics, Hungary University of Manchester, UK University of Manchester, UK --,-- Inria Paris and École Normale Supérieure, France --,-- TU Dortmund, Germany --,-- University of Tartu, Estonia University of Tartu, Estonia --,-- Charles University, Czechia Unimol, Italy --,-- --,-- University of Tehran, Tehran Institute for Advanced Studies, Iran Diffblue Ltd, United Kingdom --,-- Ca' Foscari University of Venice, Italy LMU Munich, Germany --,-- --,-- --,-- Nanjing University, China Inria and University of Lille, France Tohoku University, Japan LMU Munich, Germany Xidian University, China --,-- --,-- --,-- --,-- Tata Consultancy Services, India LMU Munich, Germany Brno University of Technology, Czechia Masaryk University, Brno, Czechia Brno University of Technology, Czechia --,-- University of Tartu, Estonia University of New South Wales, Australia LMU Munich, Germany 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 LMU Munich, Germany University of Freiburg, Germany --,-- --,-- --,--

4. SV-LIB Verification (Demo)

Ranking by Category (with Score-Based Quantile Plots)

SV-LIB.Overall 1. SvLibChecker 2. CPAchecker 3. PySvLib-CHC
Quantile plot for SV-LIB.Overall
Page 1 / 1

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 can be found in the literature [Proc. TACAS 2024, Fig. 7, page 317] and the categories are defined on the respective SV-COMP web page.

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 DASA Deagle DIVINE EBF EmergenTheta ESBMC-incr ESBMC-kind Frama-C-SV ReFuncTion Gazer-Theta GDart GDart-LLVM Goblint Goblitch Graves-CPA Hornix iekke Infer Java-Ranger JayHorn JBMC JDart JLiSA Korn Lazy-CSeq LF-checker Locksmith MLB Mopsa MuVal Nacpa OGChecker PeSCo-CPA PIChecker Pinaka PredatorHP PROTON PySvLib-CHC RacerF Re3ver SEAL SPF SV-sanitizers SVF-SVC SvLibChecker SWAT Symbiotic Theta Thorn UAutomizer UGemCutter UKojak UParalizer UTaipan VeriAbs VeriAbsL VeriOover
Representing Jury Member inactive Zhenbang Chen Nils Lommen Lei Bu inactive inactive inactive inactive Vesal Vojdani inactive inactive inactive Marek Jankola Po-Chun Chien inactive Omar Inverso Hernán Ponce de León Felix Maechtle Fei He inactive inactive Levente Bajczi Xianzhiyu Li Xianzhiyu Li inactive Naïm Moussaoui Remil inactive Malte Mues inactive Simmo Saan Karoliine Holter inactive Martin Blicha Paolo Di Biase inactive inactive Hassan Mousavi Peter Schrammel inactive Giacomo Zanatta Gidon Ernst inactive inactive inactive Lei Bu Raphaël Monat Hiroshi Unno Henrik Wachowitz Zuchao Yang inactive inactive inactive inactive Ravindra Metta Gidon Ernst Tomáš Dacík Adéla Štěpková Tomáš Dacík inactive Simmo Saan Matthew Richards Marian Lingsch-Rosenfeld Nils Loose Martin Jonáš Csanád Telbisz Levente Bajczi Matthias Heizmann Dominik Klumpp Manuel Bentele Max Barth Daniel Dietsch inactive inactive inactive
Affiliation --,-- National University of Defense Technology, China RWTH Aachen, Germany Nanjing University, China --,-- --,-- --,-- --,-- University of Tartu, Estonia --,-- --,-- --,-- LMU Munich, Germany LMU Munich, Germany --,-- Gran Sasso Science Institute, Italy Huawei Dresden Research Center, Germany University of Luebeck, Germany Tsinghua University, China --,-- --,-- Budapest University of Technology and Economics, Hungary University of Manchester, UK University of Manchester, UK --,-- Inria Paris and École Normale Supérieure, France --,-- TU Dortmund, Germany --,-- University of Tartu, Estonia University of Tartu, Estonia --,-- Charles University, Czechia Unimol, Italy --,-- --,-- University of Tehran, Tehran Institute for Advanced Studies, Iran Diffblue Ltd, United Kingdom --,-- Ca' Foscari University of Venice, Italy LMU Munich, Germany --,-- --,-- --,-- Nanjing University, China Inria and University of Lille, France Tohoku University, Japan LMU Munich, Germany Xidian University, China --,-- --,-- --,-- --,-- Tata Consultancy Services, India LMU Munich, Germany Brno University of Technology, Czechia Masaryk University, Brno, Czechia Brno University of Technology, Czechia --,-- University of Tartu, Estonia University of New South Wales, Australia LMU Munich, Germany 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 LMU Munich, Germany University of Freiburg, Germany --,-- --,-- --,--