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