Modelling & Verification 2008
Course Information


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 Ingolfsdottir, Kim 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 integrity .
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 12:00.
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.


Last modified: .