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

Here is the list of all the components that were used for executing the competition:

Repositories

Component Repository Release Tag
Verifier Archives https://gitlab.com/sosy-lab/sv-comp/archives-2022 svcomp22
Verification Tasks https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks svcomp22
Benchmark Definitions https://gitlab.com/sosy-lab/sv-comp/bench-defs svcomp22
Tool-Info Modules https://github.com/sosy-lab/benchexec 3.10
Witness Format https://github.com/sosy-lab/sv-witnesses svcomp22
BenchExec https://github.com/sosy-lab/benchexec 3.10

Reproduction Archives

Content Reproduction Archives
Verification Tasks doi:10.5281/zenodo.5831003
Competition Results doi:10.5281/zenodo.5831008
Verifiers and Validators doi:10.5281/zenodo.5959149
Verification Witnesses doi:10.5281/zenodo.5838498
BenchExec doi:10.5281/zenodo.5720267

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 2ls.zip 2ls.xml ...
AProVE C Jera Hensel RWTH Aachen, Germany aprove.zip aprove.xml ...
BRICK C Lei Bu Nanjing University, China brick.zip brick.xml ...
CBMC C Michael Tautschnig Queen Mary University of London, UK cbmc.zip cbmc.xml ...
COASTAL Java Hors Concours --, -- coastal.zip coastal.xml ...
CoVeriTeam-Verifier-AlgoSelection C Hors Concours --, -- coveriteam-verifier-algo-selection.zip coveriteam-verifier-algo-selection.xml ...
CoVeriTeam-Verifier-ParallelPortfolio C Hors Concours --, -- coveriteam-verifier-parallel-portfolio.zip coveriteam-verifier-parallel-portfolio.xml ...
CPA-BAM-BnB C Hors Concours --, -- cpa-bam-bnb.zip cpa-bam-bnb.xml ...
CPA-BAM-SMG C Anton Vasilyev ISP RAS, Russia cpa-bam-smg.zip cpa-bam-smg.xml ...
CPAchecker 2.1 C Thomas Bunk LMU Munich, Germany cpachecker.zip cpachecker.xml ...
CPALockator C Hors Concours --, -- cpa-lockator.zip cpa-lockator.xml ...
Crux C Ryan Scott Galois, USA crux.zip crux.xml ...
CSeq C Emerson Sales Gran Sasso Science Institute, Italy cseq.zip cseq.xml ...
Dartagnan C Hernán Ponce de León Bundeswehr University Munich, Germany dartagnan.zip dartagnan.xml ...
Deagle C Fei He Tsinghua University, China deagle.zip deagle.xml ...
DIVINE C Hors Concours --, -- divine.zip divine.xml ...
EBF C Fatimah Aljaafari University of Manchester, UK ebf.zip ebf.xml ...
ESBMC-incr C Hors Concours --, -- esbmc-incr.zip esbmc-incr.xml ...
ESBMC-kind C Rafael Sá Menezes University of Manchester, UK esbmc-kind.zip esbmc-kind.xml ...
Frama-C-SV C Martin Spiessl LMU Munich, Germany frama-c-sv.zip frama-c-sv.xml ...
Gazer-Theta C Hors Concours --, -- gazer-theta.zip gazer-theta.xml ...
GDart Java Falk Howar TU Dortmund, Germany gdart.zip gdart.xml ...
Goblint C Simmo Saan University of Tartu, Estonia goblint.zip goblint.xml ...
Graves-CPA C Will Leeson University of Virginia, USA graves.zip graves.xml ...
Infer C Hors Concours --, -- infer.zip infer.xml ...
Java-Ranger Java Soha Hussein University of Minnesota, USA java-ranger.zip java-ranger.xml ...
JayHorn Java Ali Shamakhi Tehran Institute for Advanced Studies, Iran jayhorn.zip jayhorn.xml ...
JBMC Java Peter Schrammel University of Sussex and Diffblue, UK jbmc.zip jbmc.xml ...
JDart Java Falk Howar TU Dortmund, Germany jdart.zip jdart.xml ...
Korn C Gidon Ernst LMU Munich, Germany korn.zip korn.xml ...
LART C Henrich Lauko Masaryk University, Brno, Czechia lart.zip lart.xml ...
Lazy-CSeq C Hors Concours --, -- lazycseq.zip lazycseq.xml ...
Locksmith C Vesal Vojdani University of Tartu, Estonia locksmith.zip locksmith.xml ...
PeSCo C Cedric Richter University of Oldenburg, Germany pesco.zip pesco.xml ...
Pinaka C Hors Concours --, -- pinaka.zip pinaka.xml ...
PredatorHP C Hors Concours --, -- predatorhp.zip predatorhp.xml ...
SESL C Xie Li Academy of Sciences, China sesl.zip sesl.xml ...
SMACK C Hors Concours --, -- smack.zip smack.xml ...
SPF Java Hors Concours --, -- spf.zip spf.xml ...
Symbiotic C Marek Chalupa Masaryk University, Brno, Czechia symbiotic.zip symbiotic.xml ...
Theta C Vince Molnár Budapest University of Technology and Economics, Hungary theta.zip theta.xml ...
UAutomizer C Matthias Heizmann University of Freiburg, Germany uautomizer.zip uautomizer.xml ...
UGemCutter C Dominik Klumpp University of Freiburg, Germany ugemcutter.zip ugemcutter.xml ...
UKojak C Frank Schüssele University of Freiburg, Germany ukojak.zip ukojak.xml ...
UTaipan C Daniel Dietsch University of Freiburg, Germany utaipan.zip utaipan.xml ...
VeriAbs C Priyanka Darke Tata Consultancy Services, India veriabs.zip veriabs.xml ...
VeriFuzz C Raveendra Kumar Medicherla Tata Consultancy Services, India verifuzz.zip verifuzz.xml ...

Validators

Tool Lang. Type Contact Affiliation Bechmark definition Publication
CPAchecker C correctness Thomas Bunk LMU Munich, Germany cpachecker-validate-correctness-witnesses.xml ...
CPAchecker C violation Thomas Bunk LMU Munich, Germany cpachecker-validate-violation-witnesses.xml ...
CPA-witness2test C violation Thomas Lemberger LMU Munich, Germany cpa-witness2test-validate-violation-witnesses.xml ...
Dartagnan C violation Hernán Ponce de León Bundeswehr University Munich, Germany dartagnan-validate-violation-witnesses.xml ...
CProver-witness2test C violation Michael Tautschnig Queen Mary University of London, UK fshell-witness2test-validate-violation-witnesses.xml ...
GWIT Java violation Falk Howar TU Dortmund University, Germany gwit-validate-violation-witnesses.xml ...
MetaVal C correctness Martin Spiessl LMU Munich, Germany metaval-validate-correctness-witnesses.xml ...
MetaVal C violation Martin Spiessl LMU Munich, Germany metaval-validate-violation-witnesses.xml ...
NITWIT C violation Jana (Philipp) Berger RWTH Aachen, Germany nitwit-validate-violation-witnesses.xml ...
Symbiotic-Witch C violation Paulína Ayaziová Masaryk University, Brno, Czechia symbiotic-witch-validate-violation-witnesses.xml ...
UAutomizer C correctness Daniel Dietsch University of Freiburg, Germany uautomizer-validate-correctness-witnesses.xml ...
UAutomizer C violation Daniel Dietsch University of Freiburg, Germany uautomizer-validate-violation-witnesses.xml ...
WIT4JAVA Java violation Tong Wu University of Manchester, UK wit4java-validate-violation-witnesses.xml ...
WitnessLint C Martin Spiessl LMU Munich, Germany witnesslint-validate-witnesses.xml ...