Modelling and Verification: Reading Material

Main Reading Material

Most of the material has been collected in the draft textbook Reactive Systems: Modelling, Specification and Verification (postscript file) by Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen and Jiri Srba. A hard copy of a draft of this book, that is currently under consideration by Cambridge University Press, will be available at the start of the course. The textbook will be revised and completed as the course progresses, and the latest version will always be available by following this link.
Errata for the book will be available here (PDF file). Note: At the moment, the link points to a non-existent file!

Further Reading Material

System Verification by Joost-Pieter Katoen.
A Note on Game Characterization of Strong and Weak Bisimilarity by Jiri Srba. [Updated Version]
An Introduction to Milner's CCS by Luca Aceto, Anna Ingólfsdóttir and Kim G. Larsen. [Updated Version]
Game Characterization of Hennessy-Milner Logic with One Recursively Defined Variable by Jiri Srba.
A short introduction to the Concurrency Workbench (English) by Hans Huttel.
En kort introduktion til Concurrency Workbench (Dansk) by Hans Huttel.
The Edinburgh Concurrency Workbench (Version 7.1) by Faron Moller, updated by Perdita Stevens.
Timed Automata: Semantics, Algorithms and Tools by Johan Bengtsson and Wang Yi.
Model Checking Real-Time Logics by Joost-Pieter Katoen.
UPPAAL in a Nutshell by Kim G. Larsen, Paul Pettersson and Wang Yi. (older version)
A Tutorial on Uppall by Gerd Behrmann, Alexandre David and Kim G. Larsen. (new UPPAAL version, recommended for reading)
An Introduction to Binary Decision Diagrams by Henrik Reif Andersen.
BDD slides by Kim G. Larsen
Formal Methods: State of the Art and Future Directions by Edmund M. Clarke and Jeannette M. Wing.

Luca Aceto, Department of of Computer Science, Reykjavík University and Aalborg University

Last modified: .