Reproducing SV-COMP Results
A description on how we make the results of the competition reproducible can be found in the competition report; the components that are listed below in the table are described in Sect. 4 "Reproducibility".
An overview over all components that were uses in the competition can be found on the reproduction page.
Verifiers
| Tool | Lang. | Jury member | Affiliation | Archive | Bechmark definition | Publication |
| Overview | Chair | Dirk Beyer | LMU Munich, Germany | |||
| 2LS | C | Viktor Malík | Brno University of Technology, Czechia | 10184626 | 2ls.xml | ... |
| aise | C | Zhenbang Chen | National University of Defense Technology, China | 10201159 | aise.xml | ... |
| BRICK | C | Lei Bu | Nanjing University, China | 10202700 | brick.xml | ... |
| Bubaak-SpLit | C | Marek Chalupa | ISTA, Austria | 10202207 | bubaak-split.xml | ... |
| Bubaak | C | Marek Chalupa | ISTA, Austria | 10202207 | bubaak.xml | ... |
| CBMC | C | Hors Concours | --, -- | 10396159 | cbmc.xml | ... |
| COASTAL | Java | Hors Concours | --, -- | 3679243 | coastal.xml | ... |
| CoVeriTeam-Verifier-AlgoSelection | C | Hors Concours | --, -- | 10213624 | coveriteam-verifier-algo-selection.xml | ... |
| CoVeriTeam-Verifier-ParallelPortfolio | C | Hors Concours | --, -- | 10213624 | coveriteam-verifier-parallel-portfolio.xml | ... |
| CPA-BAM-BnB | C | Hors Concours | --, -- | 10396208 | cpa-bam-bnb.xml | ... |
| CPA-BAM-SMG | C | Hors Concours | --, -- | 10396261 | cpa-bam-smg.xml | ... |
| CPAchecker | C | Daniel Baier | LMU Munich, Germany | 10203297 | cpachecker.xml | ... |
| CPALockator | C | Hors Concours | --, -- | 10396305 | cpa-lockator.xml | ... |
| CPV | C | Po-Chun Chien | LMU Munich, Germany | 10203472 | cpv.xml | ... |
| Crux | C | Hors Concours | --, -- | 10396721 | crux.xml | ... |
| CSeq | C | Hors Concours | --, -- | 10396733 | cseq.xml | ... |
| Dartagnan | C | Hernán Ponce de León | Huawei Dresden Research Center, Germany | 10161362 | dartagnan.xml | ... |
| Deagle | C | Fei He | Tsinghua University, China | 10207348 | deagle.xml | ... |
| DIVINE | C | Hors Concours | --, -- | 10396745 | divine.xml | ... |
| EBF | C | Fatimah Aljaafari | University of Manchester, UK | 10171482 | ebf.xml | ... |
| EmergenTheta | C | Levente Bajczi | Budapest University of Technology and Economics, Hungary | 10198872 | emergentheta.xml | ... |
| ESBMC-incr | C | Hors Concours | --, -- | 10396755 | esbmc-incr.xml | ... |
| ESBMC-kind | C | Franz Brauße | University of Manchester, UK | 10198805 | esbmc-kind.xml | ... |
| Frama-C-SV | C | Martin Spiessl | LMU Munich, Germany | 10125011 | frama-c-sv.xml | ... |
| Gazer-Theta | C | Hors Concours | --, -- | 10396776 | gazer-theta.xml | ... |
| GDart-LLVM | C | Hors Concours | --, -- | 10397137 | gdart-llvm.xml | ... |
| GDart | Java | Falk Howar | TU Dortmund, Germany | 10059535 | gdart.xml | ... |
| Goblint | C | Simmo Saan | University of Tartu, Estonia | 10202867 | goblint.xml | ... |
| Graves-Par | C | Hors Concours | University of Virginia, USA | 10397157 | graves-par.xml | ... |
| Graves-CPA | C | Hors Concours | --, -- | 10397102 | graves.xml | ... |
| Infer | C | Hors Concours | --, -- | 10079740 | infer.xml | ... |
| Java-Ranger | Java | Hors Concours | --, -- | 7467038 | java-ranger.xml | ... |
| JayHorn | Java | Hassan Mousavi | University of Tehran, Tehran Institute for Advanced Studies, Iran | 10202537 | jayhorn.xml | ... |
| JBMC | Java | Peter Schrammel | University of Sussex and Diffblue, UK | 10198951 | jbmc.xml | ... |
| JDart | Java | Hors Concours | --, -- | 10397175 | jdart.xml | ... |
| Korn | C | Gidon Ernst | LMU Munich, Germany | 10202058 | korn.xml | ... |
| Lazy-CSeq | C | Hors Concours | --, -- | 10397183 | lazycseq.xml | ... |
| LF-checker | C | Hors Concours | --, -- | 10397206 | lf-checker.xml | ... |
| Locksmith | C | Hors Concours | --, -- | 10407379 | locksmith.xml | ... |
| MLB | Java | Lei Bu | Nanjing University, China | 10210608 | mlb.xml | ... |
| Mopsa | C | Raphaël Monat | Inria and University of Lille, France | 10198570 | mopsa.xml | ... |
| PeSCo-CPA | C | Hors Concours | --, -- | 10203346 | pesco.xml | ... |
| PIChecker | C | Hors Concours | --, -- | 7471378 | pichecker.xml | ... |
| Pinaka | C | Hors Concours | --, -- | 10407406 | pinaka.xml | ... |
| PredatorHP | C | Veronika Šoková | Brno University of Technology, Czechia | 10183805 | predatorhp.xml | ... |
| PROTON | C | Ravindra Metta | TCS, India | 10185252 | proton.xml | ... |
| RELAY-SV | C | Vesal Vojdani | University of Tartu, Estonia | 10066462 | relay-sv.xml | ... |
| SPF | Java | Hors Concours | --, -- | 10407521 | spf.xml | ... |
| sv-sanitizers | C | Simmo Saan | University of Tartu, Estonia | 10091272 | sv-sanitizers.xml | ... |
| SWAT | Java | Nils Loose | University of Luebeck, Germany | 10206092 | swat.xml | ... |
| Symbiotic | C | Martin Jonáš | Masaryk University, Brno, Czechia | 10202594 | symbiotic.xml | ... |
| Theta | C | Levente Bajczi | Budapest University of Technology and Economics, Hungary | 10202679 | theta.xml | ... |
| UAutomizer | C | Matthias Heizmann | University of Freiburg, Germany | 10203545 | uautomizer.xml | ... |
| UGemCutter | C | Dominik Klumpp | University of Freiburg, Germany | 10203548 | ugemcutter.xml | ... |
| UKojak | C | Frank Schüssele | University of Freiburg, Germany | 10203546 | ukojak.xml | ... |
| UTaipan | C | Daniel Dietsch | University of Freiburg, Germany | 10203547 | utaipan.xml | ... |
| VeriAbsL | C | Priyanka Darke | Tata Consultancy Services, India | 10244458 | veriabsl.xml | ... |
| VeriAbs | C | Priyanka Darke | Tata Consultancy Services, India | 10243500 | veriabs.xml | ... |
| VeriOover | C | Hors Concours | --, -- | 10407457 | verioover.xml | ... |
Validators
| Tool | Lang. | Format | Contact | Affiliation | Archive | Bechmark definition | Publication |
| ConcurrentWitness2Test | C | Violation 1.0 | Levente Bajczi | Budapest University of Technology and Economics, Hungary | 10184336 | concurrentwitness2test.xml | ... |
| CPAchecker | C | Correctness 1.0, Correctness 2.0 | Daniel Baier | LMU Munich, Germany | 10203297 | cpachecker.xml | ... |
| CPAchecker | C | Violation 1.0, Violation 2.0 | Daniel Baier | LMU Munich, Germany | 10203297 | cpachecker.xml | ... |
| CPA-witness2test | C | Violation 1.0 | Thomas Lemberger | LMU Munich, Germany | 10203297 | cpa-witness2test.xml | ... |
| Dartagnan | C | Violation 1.0 | Hernán Ponce de León | Huawei Dresden Research Center, Germany | 10161362 | dartagnan.xml | ... |
| CProver-witness2test | C | Violation 1.0 | Hors Concours | --, -- | 10206716 | fshell-witness2test.xml | ... |
| Goblint | C | Correctness 2.0 | Simmo Saan | University of Tartu, Estonia | 10202867 | goblint.xml | ... |
| GWIT | Java | Violation 1.0 | Falk Howar | TU Dortmund, Germany | 10059567 | gwit.xml | ... |
| JCWIT | Java | Correctness 1.0 | Zaiyu Cheng | University of Manchester, UK | 10207438 | jcwit.xml | ... |
| LIV | C | Correctness 1.0 | Martin Spiessl | LMU Munich, Germany | 10202756 | liv.xml | ... |
| MetaVal | C | Correctness 1.0 | Martin Spiessl | LMU Munich, Germany | 10137150 | metaval.xml | ... |
| MetaVal | C | Violation 1.0 | Martin Spiessl | LMU Munich, Germany | 10137150 | metaval.xml | ... |
| Mopsa | C | Correctness 2.0 | Raphaël Monat | Inria and University of Lille, France | 10198570 | mopsa.xml | ... |
| NITWIT | C | Violation 1.0 | Jana (Philipp) Berger | RWTH Aachen, Germany | 10116345 | nitwit.xml | ... |
| Symbiotic-Witch | C | Violation 1.0 | Paulína Ayaziová | Masaryk University, Brno, Czechia | 10211062 | symbiotic-witch.xml | ... |
| UAutomizer | C | Correctness 1.0 | Matthias Heizmann | University of Freiburg, Germany | 10203545 | uautomizer.xml | ... |
| UAutomizer | C | Correctness 2.0 | Matthias Heizmann | University of Freiburg, Germany | 10223333 | uautomizer.xml | ... |
| UAutomizer | C | Violation 1.0 | Matthias Heizmann | University of Freiburg, Germany | 10203545 | uautomizer.xml | ... |
| WIT4JAVA | Java | Violation 1.0 | Hors Concours | --, -- | 10206747 | wit4java.xml | ... |
| Witch | C | Violation 2.0 | Paulína Ayaziová | Masaryk University, Brno, Czechia | 10064512 | witch.xml | ... |
| WitnessLint | C, Java | Correctness 1.0 | Marian Lingsch-Rosenfeld | LMU Munich, Germany | 10213801 | witnesslint.xml | ... |
| WitnessLint | C, Java | Correctness 2.0 | Marian Lingsch-Rosenfeld | LMU Munich, Germany | 10213801 | witnesslint.xml | ... |
| WitnessLint | C, Java | Violation 1.0 | Marian Lingsch-Rosenfeld | LMU Munich, Germany | 10213801 | witnesslint.xml | ... |
| WitnessLint | C, Java | Violation 2.0 | Marian Lingsch-Rosenfeld | LMU Munich, Germany | 10213801 | witnesslint.xml | ... |