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".
Verifiers
| Verifier |
Lang. |
Jury member |
Affiliation |
Archive |
Tool-info module |
Bechmark definition |
Publication |
|
Overview
|
Chair
|
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
