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.
Most of the material has been collected in the draft textbook
Reactive Systems: Modelling, Specification
and Verification (postscript file)
by Luca Aceto,
Kim Guldstrand Larsen and
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
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 :-)
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
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.
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.