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
2LS C Peter Schrammel University of Sussex, UK Download two_ls.py 2ls.xml ...
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 ...
CPA-Lockator C Pavel Andrianov ISP RAS, Russia Download cpachecker.py cpa-lockator.xml ...
CPA-Seq C Marie-Christine Jakobs LMU Munich, Germany Download cpachecker.py cpa-seq.xml ...
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 ...
ESBMC-kind C Mikhail R. Gadelha University of Southampton, UK Download esbmc.py esbmc-kind.xml ...
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 ...
JPF Java Cyrille Artho KTH, Denmark Download jpf.py jpf.xml ...
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 ...
Pinaka C Eti Chaudhary IIT Hyderabad, India Download pinaka.py pinaka.xml ...
PredatorHP C Veronika Šoková BUT, Brno, Czechia Download predatorhp.py predatorhp.xml ...
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 ...
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 ...
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 ...
VeriFuzz C Raveendra Kumar Medicherla TCS Research, India Download verifuzz.py verifuzz.xml ...
VIAP C Pritom Rajkhowa Hong Kong University of Science and Technology, China Download viap.py viap.xml ...
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