Skip navigation.
Home

Software Model Checking

Instructors

Contact

  • Students:
  • Tutors:

News

  • Those who didn't give a talk yet, please give it.
  • Those who didn't write 3 pages about the most important aspect, but wanted to to that, please do it until the 15th of april 2007.

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.

Participants

Studenten

Ahmudallah Aminy, Daniel Dietsch, Kais Haddadin, Sebastian Huber, Christine Merkel, Nicola Sheldrick, Mohannad Zalloom

Nichtstudenten

Jochen Hoenicke, Alexander Malkis, Stefan Maus, Andreas Podelski, Nassim Seghir, Martin Wehrle, Thomas Wies

Seminar program

  • 22.02.07, Thursday
    • 17:15 Meeting point is the university car park to the north-west of the SWT building 052. People who have a car and can drive arrive with their cars to the meeting point. We need four cars to get everybody in. Then we drive to Schauinsland (see the map).
    • 18:15 Arrival
    • 18:30 Dinner
  • 23.02.07, Friday
    • 8:00 - 9:00 Breakfast
    • 9:00 - 10:00 Bruno Blanchet. Introduction to Abstract Interpretation. Speaker: Kais Haddadin
    • 10:15 - 11:15 Lazy Abstraction and/or Shape Analysis. Speaker: Daniel Dietsch
    • 11:30 - 12:30 Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomas Vojnar. Programs with Lists Are Counter Automata. Speaker: Nicola Sheldrick
    • 12:45 - 13:00 SWT talks
    • 13:00 - 14:30 Lunch
    • 14:30 - 15:30 Cormac Flanagan, Partice Godefroid. Dynamic Partial-order reduction for model-checking software. Speaker: Mohannad Zalloom
    • 15:45 - 16:45 Laura Bozzelli, Salvatore La Torre, Adriano Peron. Verification of well-formed Communicating Recursive State Machines. Speaker: Christine Merkel
    • 17:00 - 18:15 Chin Soon Lee, Neil D. Jones, Amir M. Ben-Amram. The Size-Change Principle of Program Termination. Speaker: Sebastian Huber
    • 18:30 Dinner
  • 24.02.07, Saturday
    • 8:00 - 9:00 Breakfast
    • 9:00 - 10:00 Ashish Tiwari. Termination of Linear Programs. Speaker: Ahmudallah Aminy
    • 10:00 - 10:25 Thomas Wies talks.
    • 10:30 - 10:55 Alexander Malkis talks.
    • 11:00 - 11:30 Break
    • 11:30 - 11:55 Jochen Hoenicke talks.
    • 12:00 - 12:25 Martin Wehrle talks.
    • 12:30 - 12:55 Nassim Seghir talks.
    • 13:00 - 14:30 Lunch
    • 14:30 - 17:30 IF (NOT raining) THEN {GOTO Schauinsland-tower; Departure} ELSE Departure

    Remember

    • You need slippers. They won't let you into the house if you have your outdoor shoes on.
    • There is neither soap nor towels for all, take your own towel and your own piece of soap.
    • No dogs.
    • For the excursion you need warm and snow- and waterproof cloths and boots.
    • Please take your laptop and cable if you give a talk; send your slides to Alexander as soon as they are ready.
    • Assume that it's not possible no use Internet and mobile phones at Schauinsland.
    • You will have a beamer, a flipchart and an overhead projector at your disposal, but no blackboard or whiteboard.
    • If you want vegetarian meals, please tell Alexander in advance.