Lecturer: Luca Aceto (email: luca AT ru DOT is)
Course Description: The aim of this course is to introduce advanced mathematical models for the formal description and analysis of programs, with emphasis on parallel, reactive systems. The course consists of about 15 lectures. It deals with semantic models for parallel systems, and logics for the description of their properties. As part and parcel of the course material, we also introduce automatic verification tools, and hint at some of the implementation techniques underlying them.
The teaching consists of lectures interspersed with exercise classes, a mini-project and self-study. I encourage you to work in groups and discuss the course material.
The lectures take place in rooms AB2 (Mondays, 15:00-17:00) and AB3 (Wednesdays 09:00-11:00). For the details on each lecture, please consult the course overview. Room AB2 is reserved for exercise sessions on Tuesdays from 15:00 till 18:00.
Learning Outcomes: At the end of the course, you will
Reading Material: The course will be based on the book Reactive Systems: Modelling,
Specification and Verification (Cambridge University Press,
July 2007) by Anna
G. Larsen, Jiri Srba and
myself. The web page for the book at CUP is here. [Endorsements]
Some other reading material is available on-line. Feel free to suggest further reading material that you might come across by posting references, links and your summary/evaluation of the article on the course blog.
Award for the Best Reader of the Book:
As all documents of a fairly large size, despite the efforts of the
authors the textbook is likely to contain (hopefully) small errors and
typos. Should you discover any problem, check whether the problem is
already mentioned in the errata. If not,
send an email to luca AT ru DOT is. Do not forget to write the page
and line number (e.g. page 12, line 6) where the error may be found in
the textbook. I will then add the error description to the errata list and
you will be awarded 1, 2 or 3 points, depending on how serious the
problem is. In your honour, your name will be put into the errata
list and will be acknowledged in future versions of the book.
During the last lecture of the course, a small prize for the best reader of the notes (i.e. the 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 :-)
Mini Projects: During the course, you will be asked to solve
mini projects to demonstrate that you can use your theoretical
knowledge to model and verify a simple system using the verification
tools CWB and
UPPAAL. You will be given 6
supervised hours for each mini project. The mini projects are supposed
to be solved in groups of two or three students and short reports
should be delivered to the lecturer. The solutions of different groups
must be independent and sharing parts of the code or the text of
the report is strictly forbidden. Representing
somebody else's work as your own will be considered a violation of the
code of academic
Each of the mini projects will account for 15% of the final mark for the course.
Take-home Celebration: The take-home celebration (some call it
"exam" :-)) will consist of a collection of problems based on the course
material. The exam will be available electronically from the course
web page on a Monday at 09:00 and will be due the following Friday at
The take-home celebration is supposed to be solved in groups of two or three students, and you will have to return your solutions in the form of a PDF file via email to the lecturer.
The take-home exam will account for 15% of the final mark for the course.