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 components that were used for SV-COMP 2020:

Repositories

Component Repository Release Tag
Verifier Archives git@gitlab.com:sosy-lab/sv-comp/archives-2021.git svcomp21
Verification Tasks git@github.com:sosy-lab/sv-benchmarks.git svcomp21
Benchmark Definitions git@github.com:sosy-lab/sv-comp.git svcomp21
Tool-Info Modules git@github.com:sosy-lab/benchexec.git 3.6
Witness Format git@github.com/sosy-lab/sv-witnesses svcomp21
BenchExec git@github.com:sosy-lab/benchexec.git 3.6

Reproduction Archives

Content Reproduction Archives
Verification Tasks doi:10.5281/zenodo.4459126
Competition Results doi:10.5281/zenodo.4458215
Verification Witnesses doi:10.5281/zenodo.4459196
BenchExec doi:10.5281/zenodo.4317433

Participating Systems

Tool Lang. Jury member Affiliation Archive Bechmark definition System description
Overview Dirk Beyer LMU Munich, Germany
2LS C Viktor Malík BUT, Brno, Czechia Download 2ls.xml ...
BRICK C Lei Bu Nanjing University, China Download brick.xml ...
CBMC C Michael Tautschnig Queen Mary University of London, UK Download cbmc.xml ...
COASTAL Java Hors Concours -- Download coastal.xml ...
CPA-BAM-BnB C Vadim Mutilin ISP RAS, Russia Download cpa-bam-bnb.xml ...
CPAchecker C Stephan Holzner LMU Munich, Germany Download cpa-seq.xml ...
CPALockator C Pavel Andrianov ISP RAS, Russia Download cpa-lockator.xml ...
Dartagnan C Hernán Ponce de León University of the Bundeswehr Munich, Germany Download dartagnan.xml ...
DIVINE C Henrich Lauko Masaryk University, Brno, Czechia Download divine.xml ...
ESBMC-incr C Felipe R. Monteiro Amazon Web Services, USA Download esbmc-incr.xml ...
ESBMC-kind C Lucas Cordeiro University of Manchester, UK Download esbmc-kind.xml ...
Frama-C C Martin Spiessl LMU Munich, Germany Download frama-c-sv.xml ...
Gazer-Theta C Ákos Hajdu Budapest University of Technology and Economics, Hungary Download gazer-theta.xml ...
Goblint C Simmo Saan University of Tartu, Estonia Download goblint.xml ...
Java-Ranger Java Soha Hussein University of Minnesota, USA Download java-ranger.xml ...
JayHorn Java Hossein Hojjat University of Tehran, Iran Download jayhorn.xml ...
JBMC Java Peter Schrammel University of Sussex and Diffblue, UK Download jbmc.xml ...
JDart Java Falk Howar TU Dortmund, Germany Download jdart.xml ...
Korn C Gidon Ernst LMU Munich, Germany Download korn.xml ...
Lazy-CSeq C Omar Inverso Gran Sasso Science Institute, Italy Download lazycseq.xml ...
PeSCo C Cedric Richter Paderborn University, Germany Download pesco.xml ...
Pinaka C Saurabh Joshi IIT Hyderabad, India Download pinaka.xml ...
PredatorHP C Hors Concours -- Download predatorhp.xml ...
SMACK C Zvonimir Rakamaric University of Utah, USA Download smack.xml ...
SPF Java Hors Concours -- Download spf.xml ...
Symbiotic C Marek Chalupa Masaryk University, Brno, Czechia Download symbiotic.xml ...
UAutomizer C Matthias Heizmann University of Freiburg, Germany Download uautomizer.xml ...
UKojak C Dominik Klumpp University of Freiburg, Germany Download ukojak.xml ...
UTaipan C Daniel Dietsch University of Freiburg, Germany Download utaipan.xml ...
VeriAbs C Priyanka Darke Tata Consultancy Services, India Download veriabs.xml ...

Validators

Validator Contact Affiliation Archive
Validator CPAchecker Karlheinz Friedberger, Martin Spießl LMU Munich, Germany Download
Validator Ultimate Automizer Daniel Dietsch, Matthias Heizmann Univesity of Freiburg, Germany Download
Validator CPA-witness2test Matthias Dangl, Thomas Lemberger LMU Munich, Germany Download
Validator FShell-witness2test Michael Tautschnig Queen Mary University of London, UK Download
Validator MetaVal Martin Spießl LMU Munich, Germany Download
Validator NITWIT Philipp Berger RWTH Aachen, Germany Download
Validator WitnessLint Sven Umbricht LMU Munich, Germany Download