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 ...