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:
| Tool |
Lang. |
Jury member |
Affiliation |
Archive |
Bechmark definition |
Publication |
|
Overview
|
Chair
|
Dirk Beyer
|
LMU Munich, Germany
|
|
|
|
|
2LS
|
C
|
Viktor Malík
|
Brno University of Technology, Czechia
|
2ls.zip
|
2ls.xml
|
...
|
|
AProVE
|
C
|
Jera Hensel
|
RWTH Aachen, Germany
|
aprove.zip
|
aprove.xml
|
...
|
|
BRICK
|
C
|
Lei Bu
|
Nanjing University, China
|
brick.zip
|
brick.xml
|
...
|
|
CBMC
|
C
|
Michael Tautschnig
|
Queen Mary University of London, UK
|
cbmc.zip
|
cbmc.xml
|
...
|
|
COASTAL
|
Java
|
Hors Concours
|
--, --
|
coastal.zip
|
coastal.xml
|
...
|
|
CoVeriTeam-Verifier-AlgoSelection
|
C
|
Hors Concours
|
--, --
|
coveriteam-verifier-algo-selection.zip
|
coveriteam-verifier-algo-selection.xml
|
...
|
|
CoVeriTeam-Verifier-ParallelPortfolio
|
C
|
Hors Concours
|
--, --
|
coveriteam-verifier-parallel-portfolio.zip
|
coveriteam-verifier-parallel-portfolio.xml
|
...
|
|
CPA-BAM-BnB
|
C
|
Hors Concours
|
--, --
|
cpa-bam-bnb.zip
|
cpa-bam-bnb.xml
|
...
|
|
CPA-BAM-SMG
|
C
|
Anton Vasilyev
|
ISP RAS, Russia
|
cpa-bam-smg.zip
|
cpa-bam-smg.xml
|
...
|
|
CPAchecker 2.1
|
C
|
Thomas Bunk
|
LMU Munich, Germany
|
cpachecker.zip
|
cpachecker.xml
|
...
|
|
CPALockator
|
C
|
Hors Concours
|
--, --
|
cpa-lockator.zip
|
cpa-lockator.xml
|
...
|
|
Crux
|
C
|
Ryan Scott
|
Galois, USA
|
crux.zip
|
crux.xml
|
...
|
|
CSeq
|
C
|
Emerson Sales
|
Gran Sasso Science Institute, Italy
|
cseq.zip
|
cseq.xml
|
...
|
|
Dartagnan
|
C
|
Hernán Ponce de León
|
Bundeswehr University Munich, Germany
|
dartagnan.zip
|
dartagnan.xml
|
...
|
|
Deagle
|
C
|
Fei He
|
Tsinghua University, China
|
deagle.zip
|
deagle.xml
|
...
|
|
DIVINE
|
C
|
Hors Concours
|
--, --
|
divine.zip
|
divine.xml
|
...
|
|
EBF
|
C
|
Fatimah Aljaafari
|
University of Manchester, UK
|
ebf.zip
|
ebf.xml
|
...
|
|
ESBMC-incr
|
C
|
Hors Concours
|
--, --
|
esbmc-incr.zip
|
esbmc-incr.xml
|
...
|
|
ESBMC-kind
|
C
|
Rafael Sá Menezes
|
University of Manchester, UK
|
esbmc-kind.zip
|
esbmc-kind.xml
|
...
|
|
Frama-C-SV
|
C
|
Martin Spiessl
|
LMU Munich, Germany
|
frama-c-sv.zip
|
frama-c-sv.xml
|
...
|
|
Gazer-Theta
|
C
|
Hors Concours
|
--, --
|
gazer-theta.zip
|
gazer-theta.xml
|
...
|
|
GDart
|
Java
|
Falk Howar
|
TU Dortmund, Germany
|
gdart.zip
|
gdart.xml
|
...
|
|
Goblint
|
C
|
Simmo Saan
|
University of Tartu, Estonia
|
goblint.zip
|
goblint.xml
|
...
|
|
Graves-CPA
|
C
|
Will Leeson
|
University of Virginia, USA
|
graves.zip
|
graves.xml
|
...
|
|
Infer
|
C
|
Hors Concours
|
--, --
|
infer.zip
|
infer.xml
|
...
|
|
Java-Ranger
|
Java
|
Soha Hussein
|
University of Minnesota, USA
|
java-ranger.zip
|
java-ranger.xml
|
...
|
|
JayHorn
|
Java
|
Ali Shamakhi
|
Tehran Institute for Advanced Studies, Iran
|
jayhorn.zip
|
jayhorn.xml
|
...
|
|
JBMC
|
Java
|
Peter Schrammel
|
University of Sussex and Diffblue, UK
|
jbmc.zip
|
jbmc.xml
|
...
|
|
JDart
|
Java
|
Falk Howar
|
TU Dortmund, Germany
|
jdart.zip
|
jdart.xml
|
...
|
|
Korn
|
C
|
Gidon Ernst
|
LMU Munich, Germany
|
korn.zip
|
korn.xml
|
...
|
|
LART
|
C
|
Henrich Lauko
|
Masaryk University, Brno, Czechia
|
lart.zip
|
lart.xml
|
...
|
|
Lazy-CSeq
|
C
|
Hors Concours
|
--, --
|
lazycseq.zip
|
lazycseq.xml
|
...
|
|
Locksmith
|
C
|
Vesal Vojdani
|
University of Tartu, Estonia
|
locksmith.zip
|
locksmith.xml
|
...
|
|
PeSCo
|
C
|
Cedric Richter
|
University of Oldenburg, Germany
|
pesco.zip
|
pesco.xml
|
...
|
|
Pinaka
|
C
|
Hors Concours
|
--, --
|
pinaka.zip
|
pinaka.xml
|
...
|
|
PredatorHP
|
C
|
Hors Concours
|
--, --
|
predatorhp.zip
|
predatorhp.xml
|
...
|
|
SESL
|
C
|
Xie Li
|
Academy of Sciences, China
|
sesl.zip
|
sesl.xml
|
...
|
|
SMACK
|
C
|
Hors Concours
|
--, --
|
smack.zip
|
smack.xml
|
...
|
|
SPF
|
Java
|
Hors Concours
|
--, --
|
spf.zip
|
spf.xml
|
...
|
|
Symbiotic
|
C
|
Marek Chalupa
|
Masaryk University, Brno, Czechia
|
symbiotic.zip
|
symbiotic.xml
|
...
|
|
Theta
|
C
|
Vince Molnár
|
Budapest University of Technology and Economics, Hungary
|
theta.zip
|
theta.xml
|
...
|
|
UAutomizer
|
C
|
Matthias Heizmann
|
University of Freiburg, Germany
|
uautomizer.zip
|
uautomizer.xml
|
...
|
|
UGemCutter
|
C
|
Dominik Klumpp
|
University of Freiburg, Germany
|
ugemcutter.zip
|
ugemcutter.xml
|
...
|
|
UKojak
|
C
|
Frank Schüssele
|
University of Freiburg, Germany
|
ukojak.zip
|
ukojak.xml
|
...
|
|
UTaipan
|
C
|
Daniel Dietsch
|
University of Freiburg, Germany
|
utaipan.zip
|
utaipan.xml
|
...
|
|
VeriAbs
|
C
|
Priyanka Darke
|
Tata Consultancy Services, India
|
veriabs.zip
|
veriabs.xml
|
...
|
|
VeriFuzz
|
C
|
Raveendra Kumar Medicherla
|
Tata Consultancy Services, India
|
verifuzz.zip
|
verifuzz.xml
|
...
|
| Tool |
Lang. |
Type |
Contact |
Affiliation |
Bechmark definition |
Publication |
|
CPAchecker
|
C
|
correctness
|
Thomas Bunk
|
LMU Munich, Germany
|
cpachecker-validate-correctness-witnesses.xml
|
...
|
|
CPAchecker
|
C
|
violation
|
Thomas Bunk
|
LMU Munich, Germany
|
cpachecker-validate-violation-witnesses.xml
|
...
|
|
CPA-witness2test
|
C
|
violation
|
Thomas Lemberger
|
LMU Munich, Germany
|
cpa-witness2test-validate-violation-witnesses.xml
|
...
|
|
Dartagnan
|
C
|
violation
|
Hernán Ponce de León
|
Bundeswehr University Munich, Germany
|
dartagnan-validate-violation-witnesses.xml
|
...
|
|
CProver-witness2test
|
C
|
violation
|
Michael Tautschnig
|
Queen Mary University of London, UK
|
fshell-witness2test-validate-violation-witnesses.xml
|
...
|
|
GWIT
|
Java
|
violation
|
Falk Howar
|
TU Dortmund University, Germany
|
gwit-validate-violation-witnesses.xml
|
...
|
|
MetaVal
|
C
|
correctness
|
Martin Spiessl
|
LMU Munich, Germany
|
metaval-validate-correctness-witnesses.xml
|
...
|
|
MetaVal
|
C
|
violation
|
Martin Spiessl
|
LMU Munich, Germany
|
metaval-validate-violation-witnesses.xml
|
...
|
|
NITWIT
|
C
|
violation
|
Jana (Philipp) Berger
|
RWTH Aachen, Germany
|
nitwit-validate-violation-witnesses.xml
|
...
|
|
Symbiotic-Witch
|
C
|
violation
|
Paulína Ayaziová
|
Masaryk University, Brno, Czechia
|
symbiotic-witch-validate-violation-witnesses.xml
|
...
|
|
UAutomizer
|
C
|
correctness
|
Daniel Dietsch
|
University of Freiburg, Germany
|
uautomizer-validate-correctness-witnesses.xml
|
...
|
|
UAutomizer
|
C
|
violation
|
Daniel Dietsch
|
University of Freiburg, Germany
|
uautomizer-validate-violation-witnesses.xml
|
...
|
|
WIT4JAVA
|
Java
|
violation
|
Tong Wu
|
University of Manchester, UK
|
wit4java-validate-violation-witnesses.xml
|
...
|
|
WitnessLint
|
C
|
|
Martin Spiessl
|
LMU Munich, Germany
|
witnesslint-validate-witnesses.xml
|
...
|
