Modelling & Verification 2009

Welcome to the home-page for the course 'Modelling & Verification 2009' for Bachelor and Master students at the School of Computer Science at Reykjavik University.

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 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 may hint at some of the implementation techniques underlying them.

The teaching consists of lectures interspersed with exercise sessions, two mini-projects and self-study. I encourage you to work in groups and discuss the course material amongst yourselves.

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.

Exercise Sessions and Advice on Modus Operandi

Each week there will have an associated exercise sheet. I encourage you to work on the exercises in groups of two, and to discuss your solutions to them amongst yourselves. If you can explain the solutions to one another, then you really understand what is going on, and you will realize where there are gaps in your mastering of the course material. Should you get really stuck (see below), feel free to come and talk to me. Alternatively, you can send me an email with your questions, which I shall answer as soon as possible. Try to formulate your answers in writing before you come to see me, as this will help you clarify what the problems are.

The exercises will mostly be "pen and paper" ones, but I'll also suggest exercises or small projects involving the use of software tools. All the exercises will be "doable", and working them out will greatly increase your understanding of the topics covered in the course. The best advice I can give you is to spend some time on working them all out by yourselves, and to make sure you understand the solutions if the other students (or me) give you the solutions on a golden plate. Above all, don't give up if you cannot find the key to the solutions right away. Problem solving is often a matter of mental stamina as much as creativity.

You might wish to read How to Read Mathematics by Shai Simonson and Fernando Gouveau --- a collection of useful, down-to-earth tips on how to read, and learn from, mathematical texts.

These pages are currently maintained by Luca Aceto. They will be actively modified during the course period, and are currently undergoing heavy restructuring. You are invited to check them regularly during the spring term. The pages are dormant at other times. Let me know of any error you find on the course web pages.