Modelling & Verification 2009
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, two mini-projects and self-study. I encourage you to work in groups and discuss the course material.

The lectures take place each day in room K6 from 09:00 till 10:45. For the details on each lecture, please consult the course overview.


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.

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 two mini projects to demonstrate that you can use your theoretical knowledge to model and verify a simple system using the verification tools CWB or Concurrency Workbench of the New Century (CWB-NC), and UPPAAL. The mini projects are supposed to be solved in groups of two 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 30% of the final mark for the course.


Oral Exam/Celebration: The final course celebration (some call it "exam" :-)) will be oral and will be held on Friday, 15 May, starting at 09:00. A list of topics for the oral exam will be posted on the web by Sunday, 10 May, at the latest. You are expected to prepare a presentation of at most 18 minutes for each topic. At the exam, you will randomly pick one topic and deliver your presentation on it using a whiteboard. The examiners can (and will!) ask you questions during your presentation to find out how well you understand the material. You will receive the mark for the oral exam immediately after your presentation.
The oral exam will account for 40% of the final mark for the course.


Last modified: .