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 on pages 5 and 6.
| Verifier |
Jury member |
Affiliation |
Archive |
Tool-info module |
Bechmark definition |
System description |
|
2LS
|
Peter Schrammel
|
University of Oxford, UK
|
384e1bbc
|
two_ls.py
|
2ls.xml
|
|
|
AProVE
|
Jera Hensel
|
RWTH Aachen, Germany
|
68c5c5c6
|
aprove.py
|
aprove.xml
|
|
|
BLAST
|
Vadim Mutilin
|
ISPRAS, Russia
|
f4604a64
|
blast.py
|
blast.xml
|
|
|
Cascade
|
Wei Wang
|
New York University, USA
|
13416ae3
|
cascade.py
|
cascade.xml
|
|
|
CBMC
|
Michael Tautschnig
|
Queen Mary University of London, UK
|
c1da3afb
|
cbmc.py
|
cbmc.xml
|
|
|
Ceagle
|
Dexi Wang
|
Tsinghua University, China
|
e87edac9
|
ceagle.py
|
ceagle.xml
|
|
|
Ceagle-Absref
|
Guang Chen
|
Tsinghua University, China
|
8c17a0e6
|
ceagle_absref.py
|
ceagle-absref.xml
|
|
|
CIVL
|
Stephen Siegel
|
University of Delaware, USA
|
cfb5689b
|
civl.py
|
civl.xml
|
|
|
CPA-BAM
|
Karlheinz Friedberger
|
University of Passau, Germany
|
ef827b76
|
cpachecker.py
|
cpa-bam.xml
|
|
|
CPA-kInd
|
Matthias Dangl
|
University of Passau, Germany
|
ef827b76
|
cpachecker.py
|
cpa-kind.xml
|
|
|
CPA-RefSel
|
Stefan Löwe
|
University of Passau, Germany
|
052438d5
|
cpachecker.py
|
cpa-refsel.xml
|
|
|
CPA-Seq
|
CPAchecker Team
|
University of Passau, Germany
|
ef827b76
|
cpachecker.py
|
cpa-seq.xml
|
|
|
DIVINE
|
Vladimír Štill
|
Masaryk University, Czech Republic
|
227487c3
|
divine.py
|
divine.xml
|
|
|
ESBMC
|
Mikhail Ramalho
|
University of Southampton, UK
|
8663df7a
|
esbmc.py
|
esbmc.xml
|
|
|
ESBMC+DepthK
|
Lucas Cordeiro
|
Federal University of Amazonas, Brazil
|
048f4e5b
|
esbmcdepthk.py
|
esbmcdepthk.xml
|
|
|
Forest
|
Pablo Sanchez
|
University of Cantabria, Spain
|
433a9316
|
forest.py
|
forest.xml
|
|
|
Forester
|
Ondřej Lengál
|
BUT, Brno, Czech Republic
|
eefa56aa
|
forester.py
|
forester.xml
|
|
|
HIPrec
|
Quang Loc Le
|
National University, Singapore
|
7f355b85
|
hiprec.py
|
hiprec.xml
|
|
|
Impara
|
Björn Wachter
|
University of Oxford, UK
|
393b5b75
|
impara.py
|
impara.xml
|
|
|
Lazy-CSeq
|
Omar Inverso
|
Gran Sasso Science Institute, Italy
|
fb2c9bff
|
lazycseq.py
|
lazycseq.xml
|
|
|
LCTD
|
Keijo Heljanko
|
Aalto University, Finland
|
6d3c25be
|
lctd.py
|
lctd.xml
|
|
|
LPI
|
George Karpenkov
|
VERIMAG, France
|
fb7795cb
|
cpachecker.py
|
lpi.xml
|
|
|
Map2Check
|
Herbert Rocha
|
Federal University of Roraima, Brazil
|
4d4cd23a
|
map2check.py
|
map2check.xml
|
|
|
MU-CSeq
|
Gennaro Parlato
|
University of Southampton, UK
|
8434064f
|
mucseq.py
|
mucseq.xml
|
|
|
PAC-MAN
|
Ming-Hsien Tsai
|
Academia Sinica, Taiwan
|
2d837942
|
pacman.py
|
pacman.xml
|
|
|
PredatorHP
|
Tomas Vojnar
|
BUT, Brno, Czech Republic
|
09f7a494
|
predatorhp.py
|
predatorhp.xml
|
|
|
SeaHorn
|
Jorge Navas
|
NASA Ames Research Center, USA
|
c6a5651c
|
seahorn.py
|
seahorn.xml
|
|
|
Skink
|
Franck Cassez
|
Macquarie University, Sydney, Australia
|
261aec6c
|
skink.py
|
skink.xml
|
|
|
SMACK+Corral
|
Zvonimir Rakamaric
|
University of Utah, USA
|
12a9923a
|
smack.py
|
smack.xml
|
|
|
Symbiotic
|
Jan Strejček
|
Masaryk University, Czech Republic
|
62a6a604
|
symbiotic3.py
|
symbiotic3.xml
|
|
|
SymDIVINE
|
Jiří Barnat
|
Masaryk University, Czech Republic
|
f099d0b9
|
symdivine.py
|
symdivine.xml
|
|
|
UAutomizer
|
Matthias Heizmann
|
University of Freiburg, Germany
|
ddcafc27
|
ultimateautomizer.py
|
uautomizer.xml
|
|
|
UKojak
|
Daniel Dietsch
|
University of Freiburg, Germany
|
09c354f5
|
ultimatekojak.py
|
ukojak.xml
|
|
|
UL-CSeq
|
Bernd Fischer
|
University of Stellenbosch, ZA
|
5fd28e1e
|
ulcseq.py
|
ulcseq.xml
|
|
|
VVT
|
Alfons Laarman
|
TU Vienna, Austria
|
d39564d5
|
vvt.py
|
vvt.xml
|
|
