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
2LS ∅ C inactive 10184626 2ls.xml
aise C Zhenbang Chen National University of Defense Technology, China 17876286 aise.xml
AProVE (KoAT + LoAT) C Nils Lommen RWTH Aachen, Germany 17491801 aprove.xml
BRICK C Lei Bu Nanjing University, China 17630615 brick.xml
Bubaak ∅ C inactive 14205712 bubaak.xml
Bubaak-SpLit ∅ C inactive 14205712 bubaak-split.xml
CBMC ∅ C inactive 10396159 cbmc.xml
COASTAL ∅ Java inactive 3679243 coastal.xml
CoOpeRace meta C Vesal Vojdani University of Tartu, Estonia 17719057 cooperace.xml
CPA-BAM-BnB ∅ C inactive 10396208 cpa-bam-bnb.xml
CPA-BAM-SMG ∅ C inactive 10396261 cpa-bam-smg.xml
CPAchecker C, SV-LIB Marek Jankola LMU Munich, Germany 17777566 cpachecker.xml
CPALockator ∅ C inactive 10396305 cpa-lockator.xml
CPV C Po-Chun Chien LMU Munich, Germany 17693731 cpv.xml
Crux ∅ C inactive 10396721 crux.xml
CSeq C Omar Inverso Gran Sasso Science Institute, Italy 17722257 cseq.xml
Dartagnan C Hernán Ponce de León Huawei Dresden Research Center, Germany 17723884 dartagnan.xml
DASA new Java Felix Maechtle University of Luebeck, Germany 17693012 dasa.xml
Deagle C Fei He Tsinghua University, China 17636587 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 17779912 emergentheta.xml
ESBMC-incr C Xianzhiyu Li University of Manchester, UK 17741226 esbmc-incr.xml
ESBMC-kind C Xianzhiyu Li University of Manchester, UK 17741226 esbmc-kind.xml
Frama-C-SV ∅ C inactive 10125011 frama-c-sv.xml
ReFuncTion new C Naïm Moussaoui Remil Inria Paris and École Normale Supérieure, France 17525389 function-res.xml
Gazer-Theta ∅ C inactive 10396776 gazer-theta.xml
GDart Java Malte Mues Bergische Universität Wuppertal, Germany 17691525 gdart.xml
GDart-LLVM ∅ C inactive 10397137 gdart-llvm.xml
Goblint C Simmo Saan University of Tartu, Estonia 17642247 goblint.xml
Goblitch new C Karoliine Holter University of Tartu, Estonia 17661717 goblitch.xml
Graves-CPA ∅ meta C inactive 10397102 graves.xml
Hornix C Martin Blicha Charles University, Czechia 17638644 hornix.xml
iekke new C Paolo Di Biase Unimol, Italy 17708300 iekke.xml
Infer ∅ C inactive 10079740 infer.xml
Java-Ranger ∅ Java inactive 14205198 java-ranger.xml
JayHorn Java Hassan Mousavi University of Tehran and Tehran Institute for Advanced Studies, Iran 17670300 jayhorn.xml
JBMC Java Peter Schrammel Diffblue, UK 17688623 jbmc.xml
JDart ∅ Java inactive 10397175 jdart.xml
JLiSA new Java Giacomo Zanatta Ca' Foscari University of Venice, Italy 17609338 jlisa.xml
Korn C Gidon Ernst LMU Munich, Germany 17778961 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 17698944 mlb.xml
Mopsa C Raphaël Monat Inria and University of Lille, France 17696794 mopsa.xml
MuVal new C Hiroshi Unno Tohoku University, Japan 17769267 muval.xml
Nacpa meta C Henrik Wachowitz LMU Munich, Germany 17734971 nacpa.xml
OGChecker new C Zuchao Yang Xidian University, China 17374087 ogchecker.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 Consultancy Services, India 17602730 proton.xml
PySvLib-CHC new SV-LIB Gidon Ernst LMU Munich, Germany 18516554 pysvlib-chc.xml
RacerF C Tomáš Dacík Brno University of Technology, Czechia 17589798 racerf.xml
Re3ver new C Adéla Štěpková Masaryk University, Brno, Czechia 17672678 re3ver.xml
SEAL new C Tomáš Dacík Brno University of Technology, Czechia 17690232 seal.xml
SPF ∅ Java inactive 10407521 spf.xml
SVF-SVC C Matthew Richards University of New South Wales, Australia 17660355 svf-svc.xml
SvLibChecker new SV-LIB Marian Lingsch-Rosenfeld LMU Munich, Germany 18436449 svlibchecker.xml
SV-sanitizers C Simmo Saan University of Tartu, Estonia 17400380 sv-sanitizers.xml
SWAT Java Nils Loose University of Luebeck, Germany 17748741 swat.xml
Symbiotic C Martin Jonáš Masaryk University, Brno, Czechia 17698724 symbiotic.xml
Theta C Csanád Telbisz Budapest University of Technology and Economics, Hungary 17779913 theta.xml
Thorn C Levente Bajczi Budapest University of Technology and Economics, Hungary 17779911 thorn.xml
UAutomizer C Matthias Heizmann University of Freiburg, Germany 17735224 uautomizer.xml
UGemCutter C Dominik Klumpp University of Freiburg, Germany 17735380 ugemcutter.xml
UKojak C Manuel Bentele University of Freiburg, Germany 17735263 ukojak.xml
UParalizer new C Max Barth LMU Munich, Germany 17555227 uparalizer.xml
UTaipan C Daniel Dietsch University of Freiburg, Germany 17735313 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 v1 Zsófia Ádám Budapest University of Technology and Economics, Hungary 17407869 concurrentwitness2test.xml
CPAchecker ∅ C, SV-LIB Correctness v1 inactive 14203369 cpachecker.xml
CPAchecker C, SV-LIB Correctness v2, Violation v1, Violation v2 Marian Lingsch-Rosenfeld LMU Munich, Germany 17777566 cpachecker.xml
CPA-witness2test ∅ C Violation v1 inactive 10203297 cpa-witness2test.xml
Dartagnan C Violation v1 Hernán Ponce de León Huawei Dresden Research Center, Germany 17723884 dartagnan.xml
CProver-witness2test ∅ C Violation v1 inactive 10206716 fshell-witness2test.xml
Goblint C Correctness v2 Simmo Saan University of Tartu, Estonia 17642247 goblint.xml
GWIT ∅ Java Violation v1 inactive 10059567 gwit.xml
JCWIT ∅ Java Correctness v1 inactive 10207438 jcwit.xml
LIV ∅ C Correctness v1 inactive 14334835 liv.xml
LIV C Correctness v2 Marian Lingsch-Rosenfeld LMU Munich, Germany 17735544 liv.xml
MetaVal ∅ C Correctness v1, Violation v1 inactive 14170354 metaval.xml
MetaVal C Correctness v2, Violation v2 Marian Lingsch-Rosenfeld LMU Munich, Germany 17790528 metaval.xml
Mopsa C Correctness v2 Raphaël Monat Inria and University of Lille, France 17696794 mopsa.xml
NITWIT ∅ C Violation v1 inactive 10116345 nitwit.xml
PySvLib-Validator new SV-LIB SV-LIB v1 Marian Lingsch-Rosenfeld LMU Munich, Germany 18516554 pysvlib-validator.xml
Symbiotic-Witch ∅ C Violation v1 inactive 18462288 symbiotic-witch.xml
Theta C Correctness v2, Violation v2 Levente Bajczi Budapest University of Technology and Economics, Hungary 17779913 theta.xml
UAutomizer ∅ C Correctness v1 inactive 14209043 uautomizer.xml
UAutomizer C Correctness v2 Marcel Ebbinghaus University of Freiburg, Germany 17735224 uautomizer.xml
UAutomizer C Violation v1, Violation v2 Marcel Ebbinghaus University of Freiburg, Germany 17749227 uautomizer.xml
UGemCutter C Correctness v2 Dominik Klumpp University of Freiburg, Germany 17735380 ugemcutter.xml
UReferee C Correctness v2 Frank Schüssele University of Freiburg, Germany 17735453 ureferee.xml
UReferee ∅ C Correctness v1 inactive 14209067 ureferee.xml
Wit4Java Java Violation v1 Tong Wu University of Manchester, UK 18001116 wit4java.xml
Witch C Violation v2 Paulína Ayaziová Masaryk University, Brno, Czechia 17697224 witch.xml