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 svcomp18
Verification Tasks https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks svcomp18
Benchmark Definitions https://gitlab.com/sosy-lab/sv-comp/bench-defs svcomp18
Tool-Info Modules https://github.com/sosy-lab/benchexec 1.14
Witness Format https://github.com/sosy-lab/sv-witnesses svcomp18
BenchExec https://github.com/sosy-lab/benchexec 1.14

Verifiers

Verifier Jury member Affiliation Archive Tool-info module Bechmark definition System description
2LS Peter Schrammel University of Sussex, UK Download two_ls.py 2ls.xml ...
AProVE Jera Hensel RWTH Aachen University, Germany Download aprove.py aprove.xml ...
CBMC Michael Tautschnig Queen Mary University of London, UK Download cbmc.py cbmc.xml ...
CPA-BAM-BnB Vadim Mutilin ISP RAS, Moscow, Russia Download cpachecker.py cpa-bam-bnb.xml ...
CPA-BAM-Slicing Mikhail Mandrykin ISP RAS, Moscow, Russia Download cpachecker.py cpa-bam-slicing.xml ...
CPA-Seq Thomas Lemberger LMU Munich, Germany Download cpachecker.py cpa-seq.xml ...
DepthK Hussama Ismail Federal University of Amazonas, Brazil Download depthk.py depthk.xml ...
ESBMC-incr Felipe Monteiro Federal University of Amazonas, Brazil Download esbmc.py esbmc-incr.xml ...
ESBMC-kind Mikhail R. Gadelha University of Southampton, UK Download esbmc.py esbmc-kind.xml ...
Forester Martin Hruska BUT, Brno, Czech Republic Download forester.py forester.xml ...
InterpChecker Zhao Duan Xidian University, China Download cpachecker.py interpchecker.xml ...
Map2Check Herbert Oliveira Rocha Federal University of Roraima, Brazil Download map2check.py map2check.xml ...
PredatorHP Veronika Šoková BUT, Brno, Czech Republic Download predatorhp.py predatorhp.xml ...
Skink Franck Cassez Macquarie University, Australia Download skink.py skink.xml ...
Symbiotic Marek Chalupa Masaryk University, Brno, Czech Republic Download symbiotic.py symbiotic.xml ...
UAutomizer Matthias Heizmann University of Freiburg, Germany Download ultimateautomizer.py uautomizer.xml ...
UKojak Alexander Nutz University of Freiburg, Germany Download ultimatekojak.py ukojak.xml ...
UTaipan Daniel Dietsch University of Freiburg, Germany Download ultimatetaipan.py utaipan.xml ...
VeriAbs Priyanka Darke Tata Consultancy Services, India Download veriabs.py veriabs.xml ...
VIAP Pritom Rajkhowa Hong Kong University of Science and Technology, China Download viap.py viap.xml ...
Yogar-CBMC Liangze Yin National University of Defense Technology, China Download yogar-cbmc.py yogar-cbmc.xml ...

Validators

Validator Contact Affiliation Archive
Validator CPAchecker Matthias Dangl, Karlheinz Friedberger, Marie-Christine Jakobs 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