LZI - Schloss Dagstuhl - Talks + Materials of Seminar 14171

Seminar 14171
Evaluating Software Verification Systems: Benchmarks and Competitions

Dirk Beyer (Universität Passau, DE), Marieke Huisman (University of Twente, NL), Vladimir Klebanov (KIT - Karlsruhe Institute of Technology, DE), Rosemary Monahan (Nat. University of Ireland, IE)

Caveat: Due to caching problems of dynamic webpages, sometimes newly
uploaded files are not shown. Please reload the page accordingly.


Seminar Wide Materials
 lightning presentations from all participants
Slides: pdf

 Coincidence Count Dafny Solutions
Other: pdf

 Cross-tool Examples
Slides: pdf

 Coincidence Count Non-Dafny Solutions
Slides: pdf

 Competition challenge description
Other: txt

 Competition challenge code
Other: c


Aws Albarghouthi , University of Toronto

Ezio Bartocci , TU Wien

Bernhard Beckert , KIT - Karlsruher Institut für Technologie

Dirk Beyer , Universität Passau
 Competition on Software Verification
Abstracts: txt Slides: pdf Paper: pdf

 Automatic Software Verification (Overview)
Abstracts: txt Slides: pdf

 Lightening Intro
Slides: pdf


Marc Brockschmidt , Microsoft Research UK - Cambridge

David Cok , GrammaTech Inc.- Ithaca
 Demo introduction slides
Slides: pdfpdf


Gidon Ernst , Universität Augsburg

Marie Farrell , NUI Maynooth

Jean-Christophe Filliâtre , University Paris South
 The 2nd Verified Software Competition
Slides: pdf

 Demo introduction slides
Slides: pdf


Bernd Fischer , University of Stellenbosch

Alberto Griggio , Bruno Kessler Foundation - Trento

Radu Grigore , University of Oxford

Arie Gurfinkel , Carnegie Mellon University - Pittsburgh

Matthias Heizmann , Universität Freiburg

Marieke Huisman , University of Twente

Bart Jacobs , KU Leuven
 VeriFast mini-tutorial
Abstracts: txt


Alexey Khoroshilov , Russian Academy of Sciences - Moscow

Joseph Roland Kiniry , Galois - Portland

Vladimir Klebanov , KIT - Karlsruher Institut für Technologie

K. Rustan M. Leino , Microsoft Corporation - Redmond

Stefan Loewe , Universität Passau

Antoine Mine , ENS - Paris

Rosemary Monahan , NUI Maynooth
 Deductive Verification (Overview)
Slides: pdf


Wojciech Mostowski , University of Twente

Peter Mueller , ETH Zürich

Petr Mueller , Brno University of Technology

Vadim Mutilin , Russian Academy of Sciences - Moscow
 The Experience of Linux Driver Verification
Abstracts: txt Slides: pdf


Andrei Paskevich , University Paris South

Nadia Polikarpova , ETH Zürich

Arend Rensink , University of Twente

Philipp Ruemmer , Uppsala University
 Numerical Transition Systems
Slides: pdf


Andrey Rybalchenko , Microsoft Research UK - Cambridge

Gerhard Schellhorn , Universität Augsburg

Markus Schordan , LLNL - Livermore

Carsten Sinz , KIT - Karlsruher Institut für Technologie
 Tool demo introduction slide (LLBMC)
Slides: pdf


Bernhard Steffen , TU Dortmund

Jan Strejcek , Masaryk University - Brno

Michael Tautschnig , Queen Mary University of London
 Tutorial on Bounded Software Model Checking using CBMC
Abstracts: txt Slides: pdf Other: zip


Mattias Ulbrich , KIT - Karlsruher Institut für Technologie

Angela Wallenburg , Altran UK - Bath
 SPARK 2014
Slides: pdf


Philipp Wendler , Universität Passau
 Predicate Abstraction with CPAchecker
Abstracts: txt Slides: pdf


Thomas Wies , New York University

Jaco van de Pol , University of Twente


Creative Commons License
This webpage and the material that is made available on this webpage is licensed under a
Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 Unported License.

The CC by-nc-nd license allows you to copy, distribute and transmit the work under the following conditions: