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
Reproduction Archives
Verifiers
| Tool |
Lang. |
Jury member |
Affiliation |
Archive |
Bechmark definition |
Presentation |
Publication |
|
Overview
|
Chair
|
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 |
Presentation |
Publication |
|
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
|
|
|
