Contact
Teaching
 |
 |
|
| Model-Checking SS 2012 | ||
 |
 |
| News | Basic information | Content | Exercises | Slides | Links |
The following tools are used in the lecture and in the exercises.
-
Spin (Bell Labs)
-- Shell script to facilitate the LTL's handling
- SMV (CMU)
- OCaml : Downloads and resources
- Temporal Verification of Reactive Systems : Safety
- Software Model Checking : Survey
- An Axiomatic Basis for Computer Programming
- List of reference materials (mostly for the part that deals
with the verification of multi-threaded programs and LTL). The
whole literature overly exceeds the reading capacity, but it is provided anyway.
- Principles of Model Checking, by Christel Baier and Joost-Pieter Katoen
- Thread-Modular Model Checking, by Cormac Flanagan and Shaz Qadeer
- Concurrency Verification: Introduction to Compositional and Noncompositional Methods by W.-P. de Roever
- Introduction to program verification, by Krzysztof R. Apt and Ernst-R. Olderog
- Verification of Sequential and Concurrent Programs, by Krzysztof R. Apt and Ernst-R. Olderog
- Verification of Sequential and Concurrent Programs (in German), by Krzysztof R. Apt and Ernst-R. Olderog
- Susan Speer Owicki, Axiomatic Proof Techniques for Parallel Programs Ph.D. thesis, Cornell University, Ithaca, New York, July 1975. Department of Computer Science TR 75-251.
- Alexander Malkis, Cartesian Abstraction and Verification of Multithreaded Programs , PhD thesis, University of Freiburg, 2010.
- Radhia Cousot, Fondements des méthodes de preuve d'invariance et de fatalitéde programmes parallèles, PhD thesis, Institut National Polytechnique de Lorraine, 1985.