Modelling & Verification 2006
Course Information


Lecturer: Luca Aceto (email: luca AT ru DOT is, office: 507 A-wing)


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. The lectures take place in room 303. For the details on each lecture, please consult the course overview.


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 are available here (PDF file).
Some other reading material is also available on-line.

Award for the Best Reader of the Draft Book: As all documents of a fairly large size, despite the efforts of the authors the draft textbook is likely to contain (hopefully) 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 or has been corrected by the authors in the latest version of the book. 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 printed version of the textbook distributed at the start of the course, and describe briefly the nature of the mistake. 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 semester, 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 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 25% of the final mark for the course.


Exam: Individual and oral exam. The exam will consist of a 20 minute presentation with questions from the examiners on one of the topics that will be indicated on this page in due course. The topic for the exam will be selected randomly by each student at the start of the oral exam.
The oral exam will account for 60% of the final mark for the course.


Last modified: .