University of Freiburg | Faculty of Applied Sciences | Institute for Computer Science | Computer Networks and Telematics
The tele Research Group
Home         Teaching         Research        Tools         Openings        Publications





Seminar: Software Model Checking

Monday 9:00-11:00, room 00-034, building. 51.

The schedule (Notice the changes!)

Wei Wei
17 Nov, 2003
System and requirements modelling (Slides)

Prof. Dr. Stefan Leue
24 Nov, 2003
Automata based model checking (Slides)

Robert Mattmüller
1 Dec, 2003
Predicate abstraction (Slides)

Rafael Baumgartner
15 Dec, 2003
Boolean abstractions of C programs (Slides)

Michael Drescher
12 Jan, 2004
Automated abstraction refinement

Niklas Deutschmann
19 Jan, 2004
SLAM (Slides)

Stefan Spinner
26 Jan, 2004
JAVA program analysis with Bandera (Slides)


The organizational meeting will be held on Monday, October 20, 2003 at 9:00 am c.t. in room 00-034, building 51.

Model Checking is an algorithmic technique which analyzes a given system model for compliance with a given specification. When applied to software, the model represents the state transition structure of the software system to be analyzed. The specification is often given using some logic of automata formalism and expresses a property that we wish to hold of the system. While model checking has been applied very successfully in the verification of hardware systems, the application to software systems is becoming increasingly popular and commercial model checking tools start to become available.

The seminar aims at introducing the participants into the foundations and current examples of software model checking. Topics that will be addressed include (tenative listing):

  1. System modeling using state transition systems and Kripke structures.

    Edmund M. Clark, Jr. and Orna Grumberg and Doron A. Peled, Model Checking, MIT Press, 1999, Chapter 2: Modeling Systems, p. 14 - 26.

  2. Expressing requirements using automata and temporal logic.

    Doron A. Peled, Software Reliability Methods, Springer, 2003, Chapter 5.1 - 5.7: Formal Specification, p. 113-133.

  3. Automata based model checking.

    Edmund M. Clark, Jr. and Orna Grumberg and Doron A. Peled, Model Checking, MIT Press, 1999, Chapter 9: Model Checking and Automata Theory, p. 121 - 140.

  4. The model checker SPIN.

    Gerard J. Holzmann, The Model Checker Spin, IEEE Transactions on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295. PDF

  5. Verisoft.

    Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Bell Labs Technical Memorandum ITD-03-44189G, March 2003. To appear in a special issue of the journal "Formal Methods in System Design" on software model checking. PS

  6. Predicate abstraction.

    S. Graf and H. Saidi, Construction of Abstract State Graphs with PVS, Proceedings of CAV'97, LNCS, vol. 1254, pp. 72-83, Springer Verlag, 1997. PDF

  7. Boolean abstractions of C programs.

    Boolean and Cartesian Abstractions for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani, TACAS 2001, LNCS 2031, April 2001, pp. 268-283. PS

    Bebop: A Symbolic Model Checker for Boolean Programs, Thomas Ball, Sriram K. Rajamani, SPIN 2000 Workshop on Model Checking of Software LNCS 1885, August/September 2000, pp. 113-130. PDF

  8. Automated abstraction refinement.

    Generating Abstract Explanations of Spurious Counterexamples in C Programs, Thomas Ball, Sriram K. Rajamani, MSR-TR-2002-09. PDF

    Relative Completeness of Abstraction Refinement for Software Model Checking, Thomas Ball, Andreas Podelski, Sriram K. Rajamani, TACAS 2002, LNCS 2280, April 2002, pp. 158-172. PS

  9. SLAM.

    Automatically Validating Temporal Safety Properties of Interfaces, Thomas Ball, Sriram K. Rajamani, SPIN 2001, Workshop on Model Checking of Software, LNCS 2057, May 2001, pp. 103-122. PDF

  10. FeaVer.

    Gerard Holzmann and Margaret Smith, Automating Software Feature Verification, Bell Labs Technical Journal, Vol. 5, No. 2, April-June 2000, pp. 72-87. PDF

  11. Verification of Flight Software

    Gerard Holzmann, and Peter Gluck, Using Spin Model Checking for Flight Software Verification, Proc. 2002 Aerospace Conference, Big Sky, MT, USA, IEEE, March 2002. PDF

  12. JAVA program analysis with Bandera.

    Matthew Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina Pasareanu, Robby, Willem Visser, Hongjun Zheng, Tool-supported Program Abstraction for Finite-state Verification, in: Proceedings of the 23rd International Conference on Software Engineering, May, 2001. PDF

  13. Static Analysis and Model Checking.

    G. Brat and W. Visser, Combining Static Analysis and Model Checking for Software Analysis, Proceedings of ASE2001. San Diego, November 2001. .ps.gz



The seminar will be held in English, participants may deliver their paper presentations in German. To obtain a "Schein" or a graded credit participants need to give a 30-45 min. presentation of one of the above topics and submit a written 5-10 page summary report (in English or German).