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