Reproducing SV-COMP Results
A description on how we make the results of the competition reproducible
can be found in the
2017 competition report;
the components that are listed below in the table are described in Sect. 4 "Reproducibility".
An overview over all components that were uses in the competition can be found on the
reproduction page.
In the below listings, we use superscript labels to indicate
new tools new,
inactive tools ∅, and
meta tools meta.
Tools for Verification
| Tool |
Lang. |
Jury member |
Affiliation |
Archive |
Benchmark definition |
|
Overview
|
Chair
|
Dirk Beyer
|
LMU Munich, Germany
|
|
|
|
|
2LS
|
C
|
Viktor Malík
|
Brno University of Technology, Czechia
|
10184626
|
2ls.xml
|
|
aise
|
C
|
Zhenbang Chen
|
National University of Defense Technology, China
|
14203693
|
aise.xml
|
|
AProVE (KoAT + LoAT)
|
C
|
Nils Lommen
|
RWTH Aachen, Germany
|
14192730
|
aprove.xml
|
|
BRICK
|
C
|
Lei Bu
|
Nanjing University, China
|
14203153
|
brick.xml
|
|
Bubaak
|
C
|
Marek Chalupa
|
ISTA, Austria
|
14205712
|
bubaak.xml
|
|
Bubaak-SpLit
|
C
|
Marek Chalupa
|
ISTA, Austria
|
14205712
|
bubaak-split.xml
|
|
CBMC ∅
|
C
|
inactive |
|
10396159
|
cbmc.xml
|
|
COASTAL ∅
|
Java
|
inactive |
|
3679243
|
coastal.xml
|
|
CoOpeRace meta new
|
C
|
Vesal Vojdani
|
University of Tartu, Estonia
|
14509733
|
cooperace.xml
|
|
CPA-BAM-BnB ∅
|
C
|
inactive |
|
10396208
|
cpa-bam-bnb.xml
|
|
CPA-BAM-SMG ∅
|
C
|
inactive |
|
10396261
|
cpa-bam-smg.xml
|
|
CPAchecker
|
C
|
Marian Lingsch-Rosenfeld
|
LMU Munich, Germany
|
14203369
|
cpachecker.xml
|
|
CPALockator ∅
|
C
|
inactive |
|
10396305
|
cpa-lockator.xml
|
|
CPV
|
C
|
Po-Chun Chien
|
LMU Munich, Germany
|
14203582
|
cpv.xml
|
|
Crux ∅
|
C
|
inactive |
|
10396721
|
crux.xml
|
|
CSeq ∅
|
C
|
inactive |
|
10396733
|
cseq.xml
|
|
Dartagnan
|
C
|
Hernán Ponce de León
|
Huawei Dresden Research Center, Germany
|
14079770
|
dartagnan.xml
|
|
Deagle
|
C
|
Fei He
|
Tsinghua University, China
|
14189745
|
deagle.xml
|
|
DIVINE ∅
|
C
|
inactive |
|
10396745
|
divine.xml
|
|
EBF ∅
|
C
|
inactive |
|
10171482
|
ebf.xml
|
|
EmergenTheta
|
C
|
Levente Bajczi
|
Budapest University of Technology and Economics, Hungary
|
14194484
|
emergentheta.xml
|
|
ESBMC-incr
|
C
|
Tong Wu
|
University of Manchester, UK
|
14185854
|
esbmc-incr.xml
|
|
ESBMC-kind
|
C
|
Tong Wu
|
University of Manchester, UK
|
14185854
|
esbmc-kind.xml
|
|
Frama-C-SV ∅
|
C
|
inactive |
|
10125011
|
frama-c-sv.xml
|
|
Gazer-Theta ∅
|
C
|
inactive |
|
10396776
|
gazer-theta.xml
|
|
GDart
|
Java
|
Falk Howar
|
TU Dortmund, Germany
|
14207413
|
gdart.xml
|
|
GDart-LLVM ∅
|
C
|
inactive |
|
10397137
|
gdart-llvm.xml
|
|
Goblint
|
C
|
Simmo Saan
|
University of Tartu, Estonia
|
14054652
|
goblint.xml
|
|
Graves-CPA ∅ meta
|
C
|
inactive |
|
10397102
|
graves.xml
|
|
Hornix new
|
C
|
Martin Blicha
|
University of Lugano, Switzerland
|
14208262
|
hornix.xml
|
|
Infer ∅
|
C
|
inactive |
|
10079740
|
infer.xml
|
|
Java-Ranger
|
Java
|
Soha Hussein
|
Ain Shams University, Egypt
|
14205198
|
java-ranger.xml
|
|
JayHorn ∅
|
Java
|
inactive |
|
10202537
|
jayhorn.xml
|
|
JBMC
|
Java
|
Peter Schrammel
|
Diffblue, UK
|
14207455
|
jbmc.xml
|
|
JDart ∅
|
Java
|
inactive |
|
10397175
|
jdart.xml
|
|
Korn
|
C
|
Gidon Ernst
|
LMU Munich, Germany
|
13987882
|
korn.xml
|
|
Lazy-CSeq ∅
|
C
|
inactive |
|
10397183
|
lazycseq.xml
|
|
LF-checker ∅
|
C
|
inactive |
|
10397206
|
lf-checker.xml
|
|
Locksmith ∅
|
C
|
inactive |
|
10407379
|
locksmith.xml
|
|
MLB
|
Java
|
Lei Bu
|
Nanjing University, China
|
14229077
|
mlb.xml
|
|
Mopsa
|
C
|
Raphaël Monat
|
Inria and University of Lille, France
|
14208644
|
mopsa.xml
|
|
Nacpa meta new
|
C
|
Henrik Wachowitz
|
LMU Munich, Germany
|
14203473
|
nacpa.xml
|
|
PeSCo-CPA ∅ meta
|
C
|
inactive |
|
10203346
|
pesco.xml
|
|
PIChecker ∅
|
C
|
inactive |
|
7471378
|
pichecker.xml
|
|
Pinaka ∅
|
C
|
inactive |
|
10407406
|
pinaka.xml
|
|
PredatorHP ∅
|
C
|
inactive |
|
10183805
|
predatorhp.xml
|
|
PROTON
|
C
|
Ravindra Metta
|
Tata Consulting Services, India
|
14209458
|
proton.xml
|
|
RacerF new
|
C
|
Tomáš Dacík
|
Brno University of Technology, Czechia
|
14507645
|
racerf.xml
|
|
SPF ∅
|
Java
|
inactive |
|
10407521
|
spf.xml
|
|
SVF-SVC new
|
C
|
Matthew Richards
|
University of New South Wales, Australia
|
14208597
|
svf-svc.xml
|
|
sv-sanitizers
|
C
|
Simmo Saan
|
University of Tartu, Estonia
|
14172703
|
sv-sanitizers.xml
|
|
SWAT
|
Java
|
Nils Loose
|
University of Luebeck, Germany
|
14214662
|
swat.xml
|
|
Symbiotic
|
C
|
Martin Jonáš
|
Masaryk University, Brno, Czechia
|
14230101
|
symbiotic.xml
|
|
Theta
|
C
|
Levente Bajczi
|
Budapest University of Technology and Economics, Hungary
|
14194483
|
theta.xml
|
|
Thorn new
|
C
|
Levente Bajczi
|
Budapest University of Technology and Economics, Hungary
|
14194485
|
thorn.xml
|
|
UAutomizer
|
C
|
Matthias Heizmann
|
University of Freiburg, Germany
|
14209043
|
uautomizer.xml
|
|
UGemCutter
|
C
|
Dominik Klumpp
|
University of Freiburg, Germany
|
14209054
|
ugemcutter.xml
|
|
UKojak
|
C
|
Manuel Bentele
|
University of Freiburg, Germany
|
14209044
|
ukojak.xml
|
|
UTaipan
|
C
|
Daniel Dietsch
|
University of Freiburg, Germany
|
14209053
|
utaipan.xml
|
|
VeriAbsL ∅
|
C
|
inactive |
|
10244458
|
veriabsl.xml
|
|
VeriAbs ∅
|
C
|
inactive |
|
10243500
|
veriabs.xml
|
|
VeriOover ∅
|
C
|
inactive |
|
10407457
|
verioover.xml
|
Tools for Validation
| Tool |
Lang. |
Format |
Jury member |
Affiliation |
Archive |
Benchmark definition |
|
ConcurrentWitness2Test
|
C
|
Violation 1.0
|
Zsófia Ádám
|
Budapest University of Technology and Economics, Hungary
|
14063728
|
concurrentwitness2test.xml
|
|
CPAchecker
|
C
|
Correctness 1.0, Correctness 2.0, Violation 1.0, Violation 2.0
|
Marian Lingsch-Rosenfeld
|
LMU Munich, Germany
|
14203369
|
cpachecker.xml
|
|
CPA-witness2test ∅
|
C
|
Violation 1.0
|
inactive |
|
10203297
|
cpa-witness2test.xml
|
|
Dartagnan
|
C
|
Violation 1.0
|
Hernán Ponce de León
|
Huawei Dresden Research Center, Germany
|
14079770
|
dartagnan.xml
|
|
CProver-witness2test ∅
|
C
|
Violation 1.0
|
inactive |
|
10206716
|
fshell-witness2test.xml
|
|
Goblint
|
C
|
Correctness 2.0
|
Simmo Saan
|
University of Tartu, Estonia
|
14054652
|
goblint.xml
|
|
GWIT ∅
|
Java
|
Violation 1.0
|
inactive |
|
10059567
|
gwit.xml
|
|
JCWIT ∅
|
Java
|
Correctness 1.0
|
inactive |
|
10207438
|
jcwit.xml
|
|
LIV
|
C
|
Correctness 2.0, Correctness 1.0
|
Marian Lingsch-Rosenfeld
|
LMU Munich, Germany
|
14334835
|
liv.xml
|
|
MetaVal
|
C
|
Correctness 1.0, Correctness 2.0, Violation 1.0, Violation 2.0
|
Marian Lingsch-Rosenfeld
|
LMU Munich, Germany
|
14170354
|
metaval.xml
|
|
MetaVal++ new
|
C
|
Correctness 2.0
|
Marian Lingsch-Rosenfeld
|
LMU Munich, Germany
|
14194293
|
metaval++.xml
|
|
Mopsa
|
C
|
Correctness 2.0
|
Raphaël Monat
|
Inria and University of Lille, France
|
14208644
|
mopsa.xml
|
|
NITWIT ∅
|
C
|
Violation 1.0
|
inactive |
|
10116345
|
nitwit.xml
|
|
Symbiotic-Witch
|
C
|
Violation 1.0
|
Paulína Ayaziová
|
Masaryk University, Brno, Czechia
|
14207464
|
symbiotic-witch.xml
|
|
UAutomizer
|
C
|
Correctness 1.0, Correctness 2.0, Violation 1.0, Violation 2.0
|
Marcel Ebbinghaus
|
University of Freiburg, Germany
|
14209043
|
uautomizer.xml
|
|
UReferee new
|
C
|
Correctness 1.0, Correctness 2.0
|
Frank Schüssele
|
University of Freiburg, Germany
|
14209067
|
ureferee.xml
|
|
Wit4Java
|
Java
|
Violation 1.0
|
Tong Wu
|
University of Manchester, UK
|
14261105
|
wit4java.xml
|
|
Witch
|
C
|
Violation 2.0
|
Paulína Ayaziová
|
Masaryk University, Brno, Czechia
|
14207188
|
witch.xml
|
