Semantics & Verification, Spring 2005

Online Reading Material

Semantics & Verification, Spring 2005

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 Uppsala.
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.

The above reading material has been collected in two compendiums (Semantics & Verification 2004 by L. Aceto, and Semantics & Verification 2005 by J. Srba). They can be bought at the bookshop in building B. I do recommend to get both of them.

Errata

Language (non-technical) typos are not in the errata lists but they are fixed in the updated version of the documents. The following points were awarded for language typos so far: Lasse Bigum (1.5 points), Peter Sönder (0.25 points), Jakob Olesen (1 point), Loic Cerf (0.5 points).

Award for the Best Reader of the Notes

The second and third lecture notes (game characterization of bisimilarity and introduction to Milner's CCS) are used for the first time in its current form and are therefore likely to contain small errors and typos. Should you discover any problem (e.g. a missing index, inconsistent notation or a spelling error), check whether the problem is already mentioned in the errata and if not, send an email to srba@cs.aau.dk. Do not forget to write the page and line number (e.g. page 12, line 6) and describe briefly the error. I will then place the error description to the errata list and you will be awarded 1, 2 or 3 points, depending on how serious the problem is. For your honour, your name will be put into the errata list. During the last lecture of the course, a prize for the best reader of the notes (i.e. a student with maximum total number of points) will be awarded. Details about the prize will be specified later on but it will be definitely worth the effort :-)