|
TACAS |
| 15th Competition on Software Verification (SV-COMP 2026) | |
Results of the Competition on Witness Validation
This web page presents the results of SV-COMP 2026 - 15th International Competition on Software Verification
-
Competition Report of SV-COMP 2026
- The benchmarks and rules are also available from the competition website.
- Results of the Verification Track are also available.
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.
1. Validation of Correctness Witnesses v2
Ranking by Category (with Score-Based Quantile Plots)
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 | CPAchecker | Goblint | LIV | MetaVal | Mopsa | Theta | UAutomizer | UGemCutter | UReferee |
|---|---|---|---|---|---|---|---|---|---|---|
| Representing Jury Member | Marian Lingsch-Rosenfeld | Simmo Saan | Marian Lingsch-Rosenfeld | Marian Lingsch-Rosenfeld | Raphaël Monat | Levente Bajczi | Marcel Ebbinghaus | Dominik Klumpp | Frank Schüssele | |
| Affiliation | LMU Munich, Germany | University of Tartu, Estonia | LMU Munich, Germany | LMU Munich, Germany | Inria and University of Lille, France | Budapest University of Technology and Economics, Hungary | University of Freiburg, Germany | LIX - CNRS - École Polytechnique, France | University of Freiburg, Germany |
2. Validation of Violation Witnesses v2
Ranking by Category (with Score-Based Quantile Plots)
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 | CPAchecker | MetaVal | Theta | UAutomizer | Witch |
|---|---|---|---|---|---|---|
| Representing Jury Member | Marian Lingsch-Rosenfeld | Marian Lingsch-Rosenfeld | Levente Bajczi | Marcel Ebbinghaus | Paulína Ayaziová | |
| Affiliation | LMU Munich, Germany | LMU Munich, Germany | Budapest University of Technology and Economics, Hungary | University of Freiburg, Germany | Masaryk University, Brno, Czechia |
3. Validation of Violation Witnesses v1
Ranking by Category (with Score-Based Quantile Plots)
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 | ConcurrentWitness2Test | CPA-witness2test | CPAchecker | Dartagnan | CProver-witness2test | GWIT | MetaVal | NITWIT | Symbiotic-Witch | UAutomizer | Wit4Java |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Representing Jury Member | Zsófia Ádám | inactive | Marian Lingsch-Rosenfeld | Hernán Ponce de León | inactive | inactive | inactive | inactive | inactive | Marcel Ebbinghaus | Tong Wu | |
| Affiliation | Budapest University of Technology and Economics, Hungary | --,-- | LMU Munich, Germany | Huawei Dresden Research Center, Germany | --,-- | --,-- | --,-- | --,-- | --,-- | University of Freiburg, Germany | University of Manchester, UK |