LZI - Schloss Dagstuhl - Talks + Materials of Seminar 14171
 Functions: 

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
 



License

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: