Participants of the Competition
(This is not a ranking, the list is in order of submission.)
System descriptions and tool-package archives can be found below under Competition Candidates. References to the published papers are listed in the last section.
-
Predator 2011-10-11
Kamil Dudka, Petr Muller, Petr Peringer, and Tomas Vojnar
Brno University of Technology, Czech Republic -
BLAST 2.7
Pavel Shved, Vadim Mutilin, and Mikhail Mandrykin
Russian Academy of Sciences, Russia -
CPAchecker-Memorizing 1.0.10
Daniel Wonisch
University of Paderborn, Germany -
ESBMC 1.17
Lucas Cordeiro, Jeremy Morse, Denis Nicole, and Bernd Fischer
University of Southampton, UK -
LLBMC 0.9
Carsten Sinz, Stephan Falke, and Florian Merz
Karlsruhe Institute of Technology, Germany -
Wolverine 0.5c
Georg Weissenbacher, Daniel Kroening, and Sharad Malik
Princeton University, USA -
CPAchecker-ABE 1.0.10
Stefan Löwe and Philipp Wendler
University of Passau, Germany -
SATabs 3.0
Alastair Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, and Thomas Wahl
Oxford University, UK -
FShell 1.3
Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, and Helmut Veith
TU Vienna, Austria -
QARMC-HSF
Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko
TU Munich, Germany
Competition Candidates
In order to ensure reproducibility of the competition results, the following table provides the original tool packages and the original system descriptions (published final papers in the next section).
| Candidate | Tool | Tool SHA | Paper | Paper SHA |
| Predator 2011-10-11 | predator-2011-10-11-8a7846b.tar.gz | b4b14db6ab4ba01bae2f4bc848c143dc650b193e | tacas2012_submission_197_Predator: A Verification Tool for Programs with Dynamic Linked Data Structures.pdf | 43f3a06751bbdd65b1d955e902f5d1014f2e0ad6 |
| BLAST 2.7 | blast-2.7-bin-x86_64.tgz | c7b2ac22677af8e644274be0432a64f43161ddef | tacas2012_submission_199_BLAST 2.7.pdf | c1e5ae69c5f6b2b224fa562d1e65a721838b8456 |
| CPAchecker-Memorizing 1.0.10 | cpachecker-abm.zip | e2729a14504479eb2fef0cb0f92d337683acdf6a | tacas2012_submission_200_Adjustable Block Memorization for CPAchecker.pdf | 92a253f7cd0f6ecb997bac229f0e1e45748570e2 |
| ESBMC 1.17 | esbmc-v1.17-linux-64.tar.gz | 42dc762510a7fcbbec69aed237491427e0c1c8b5 | tacas2012_submission_201_TACAS'12 Competition Entry: ESBMC v1.17.pdf | e7edad3a6fec333e1eac0a85f642ec848f8b8a0a |
| LLBMC 0.9 | llbmc-tacas12.zip | d09a39e24b36e24a09a28b2b8c57553569ec1e0e | tacas2012_submission_202_LLBMC: A Bounded Model Checking for LLVM's Intermediate Representation.pdf | 035ec0c1af3af1fb072fb9e218f8cb38601b538b |
| Wolverine 0.5c | wolverine.Linux_x86_64.tgz | 83f5fb0f6e790d8ada8ec019c3fdac2ef4351dee | tacas2012_submission_203_WOLVERINE: Battling Bugs with Interpolants.pdf | 7381b414bafd4dc28a8a673b4e220de7035e1220 |
| CPAchecker-ABE 1.0.10 | cpachecker_sv-comp12.zip | d6f0b27e83183422c2f8cb8ee06fcb3094cfd0a8 | tacas2012_submission_204_CPAchecker with Dynamically Adjustable Predicate Analysis.pdf | 2b0882681751c52930e4e84431b07ef896d2de3c |
| SATabs 3.0 | satabs.20111013.2200.tar.bz2 | 20608a7afc2fe2c01b088c43ff72b985c2ef2123 | tacas2012_submission_205_Symmetry-Aware SATABS.pdf | 2d8c7d49b6cc89c77a63ef95a293f1300a3d9dcd |
| FShell 1.3 | fshell2-1.3-x86_64-linux-gnu.tar.gz | 74abfacfed2ad1ae6ccea284aa6802d556c5905d | tacas2012_submission_206_FShell.pdf | baf13877d4b281071e4b6eacf1cefcfc403aa9e6 |
| QARMC-HSF | hsf-dist.tar.bz2 | 6ba8d8651d8c4b53e4aa1876666559fea88cebc3 | tacas2012_submission_207_HSF: A Software Verifier based on Horn clauses.pdf | 1b7877fee6813d25a81a8ce43530995e7e00f6c7 |
References
The following list links to the final papers as published in the TACAS proceedings (taken from the TACAS Proceedings at DBLP).
- Dirk Beyer:
Competition on Software Verification - (SV-COMP). 504-524
- Pavel Shved, Mikhail Mandrykin, Vadim Mutilin:
Predicate Analysis with BLAST 2.7 - (Competition Contribution). 525-527
- Stefan Löwe, Philipp Wendler:
CPAchecker with Adjustable Predicate Analysis - (Competition Contribution). 528-530
- Daniel Wonisch:
Block Abstraction Memoization for CPAchecker - (Competition Contribution). 531-533
- Lucas Cordeiro, Jeremy Morse, Denis Nicole, Bernd Fischer:
Context-Bounded Model Checking with ESBMC 1.17 - (Competition Contribution). 534-537
- Andreas Holzer, Daniel Kroening, Christian Schallhart, Michael Tautschnig, Helmut Veith:
Proving Reachability Using FShell - (Competition Contribution). 538-541
- Carsten Sinz, Florian Merz, Stephan Falke:
LLBMC: A Bounded Model Checker for LLVM's Intermediate Representation - (Competition Contribution). 542-544
- Kamil Dudka, Petr Müller, Petr Peringer, Tomás Vojnar:
Predator: A Verification Tool for Programs with Dynamic Linked Data Structures - (Competition Contribution). 545-548
- Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, Andrey Rybalchenko:
HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). 549-551
- Gérard Basler, Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, Thomas Wahl:
SATabs: A Bit-Precise Verifier for C Programs - (Competition Contribution). 552-555
- Georg Weissenbacher, Daniel Kroening, Sharad Malik:
Wolverine: Battling Bugs with Interpolants - (Competition Contribution). 556-558