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

Verifier Lang. Jury member Affiliation Archive Tool-info module Bechmark definition System description
Overview Dirk Beyer LMU Munich talk
2LS C Peter Schrammel University of Sussex, UK Download two_ls.py 2ls.xml talk
AProVE C Jera Hensel RWTH Aachen, Germany Download aprove.py aprove.xml ...
CBMC C Michael Tautschnig Amazon Web Services, UK Download cbmc.py cbmc.xml ...
CBMC-Path C Kareem Khazem University College London, UK Download cbmc-path.py cbmc-path.xml ...
CPA-BAM-BnB C Vadim Mutilin ISP RAS, Russia Download cpachecker.py cpa-bam-bnb.xml talk
CPA-Lockator C Pavel Andrianov ISP RAS, Russia Download cpachecker.py cpa-lockator.xml talk
CPA-Seq C Marie-Christine Jakobs LMU Munich, Germany Download cpachecker.py cpa-seq.xml talk
DepthK C Omar Alhawi University of Manchester, UK Download depthk.py depthk.xml ...
DIVINE-explicit C Vladimír Štill Masaryk University, Czechia Download divine4.py divine-explicit.xml ...
DIVINE-SMT C Henrich Lauko Masaryk University, Czechia Download divine4.py divine-smt.xml talk
ESBMC-kind C Mikhail R. Gadelha University of Southampton, UK Download esbmc.py esbmc-kind.xml talk
JayHorn Java Philipp Ruemmer Uppsala University, Sweden Download jayhorn.py jayhorn.xml ...
JBMC Java Lucas Cordeiro University of Manchester, UK Download jbmc.py jbmc.xml talk
JPF Java Cyrille Artho KTH, Sweden Download jpf.py jpf.xml talk
Lazy-CSeq C Omar Inverso Gran Sasso Science Institute, Italy Download cseq.py lazycseq.xml ...
Map2Check C Herbert Rocha Federal University of Roraima, Brazil Download map2check.py map2check.xml ...
PeSCo C Cedric Richter University of Paderborn, Germany Download pesco.py pesco.xml talk
Pinaka C Eti Chaudhary IIT Hyderabad, India Download pinaka.py pinaka.xml talk
PredatorHP C Veronika Šoková BUT, Brno, Czechia Download predatorhp.py predatorhp.xml talk
Skink C Franck Cassez Macquarie University, Australia Download skink.py skink.xml ...
SMACK C Zvonimir Rakamaric University of Utah, USA Download smack.py smack.xml talk
SPF Java Willem Visser Stellenbosch University, South Africa Download spf.py spf.xml ...
Symbiotic C Marek Chalupa Masaryk University, Czechia Download symbiotic.py symbiotic.xml talk
UAutomizer C Matthias Heizmann University of Freiburg, Germany Download ultimateautomizer.py uautomizer.xml ...
UKojak C Alexander Nutz University of Freiburg, Germany Download ultimatekojak.py ukojak.xml ...
UTaipan C Daniel Dietsch University of Freiburg, Germany Download ultimatetaipan.py utaipan.xml ...
VeriAbs C Priyanka Darke Tata Consultancy Services, India Download veriabs.py veriabs.xml talk
VeriFuzz C Raveendra Kumar Medicherla Tata Consultancy Services, India Download verifuzz.py verifuzz.xml talk
VIAP C Pritom Rajkhowa Hong Kong University of Science and Technology, China Download viap.py viap.xml talk
Yogar-CBMC C Liangze Yin National University of Defense Technology, China Download yogar-cbmc.py yogar-cbmc.xml ...
Yogar-CBMC-Parallel C Haining Feng National University of Defense Technology, China Download yogar-cbmc-parallel.py yogar-cbmc-parallel.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