Advanced Topic in Model-Checking, SS 2008

Instructors

• Prof. Dr. Andreas Podelski
• Dr. Harald Fecher
• Dr. Jochen Hoenicke
• Thomas Wies
  

Description

Software Model Checking deals with automated verification of programs. A variety of successful tools have emerged in the recent years, some of them have found application in the industry. We are going to learn about Software Model Checking: read papers about underlying methods and algorithms, play with tools, discuss in the class, find out what could be done better.

Registration

Please write directly to Harald, Jochen, or Thomas.

Topic list

includes, but is not limited to the following articles from TACAS 2008. To get a topic please talk to Harald, Jochen, or Thomas. These paper can be downloaded from http://www.springerlink.com/content/m74vt7q51451/

• Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
  Efficient Interpolant Generation in Satisfiability Modulo Theories. 397-412
  [assigned to Juergen Christ]
• Edmund M. Clarke, Muralidhar Talupur, Helmut Veith:
  Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. 33-47
• Adam Bakewell, Dan R. Ghica:
  On-the-Fly Techniques for Game-Based Software Model Checking. 78-92
• Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar:
  Computing Simulations over Tree Automata. 93-108
• Sebastian Kupferschmid, Jörg Hoffmann, Kim Guldstrand Larsen:
  Fast Directed Model Checking Via Russian Doll Abstraction. 203-217
• Amir M. Ben-Amram, Michael Codish:
  A SAT-Based Approach to Size Change Termination with Global Ranking Functions. 218-232
  [assigned to Fernando Meyer]
• Carsten Ihlemann, Swen Jacobs, Viorica Sofronie-Stokkermans:
  On Local Reasoning in Verification. 265-281
• Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, Sriram K. Rajamani:
  Automatically Refining Abstract Interpretations. 443-458

Talk

All the speakers are supposed to give a talk in English. The format of the slides does not matter as long as it can be presented on a standard Windows or Linux machine. We advise ps/pdf (or overhead slides). For a seminar talk, the talk length should be 40-45 minutes (plus at most 15 minutes for questions and comments from the listeners). Please send your slides to your supervising tutor so that we could look through all of them in advance.

Date & Location

The seminar will take place on as a block after the term. It will presumably take place in September or October. Details will be posted here when they are fixed.