Formal Methods is a 7.5-point (högskolepoäng) course. It is elective for D4 and IT4, but can also be read by others who are interested, such as graduate students.

Formal methods are about rigorous verification of systems. That is, techniques that can help bring about better confidence in the systems we develop and use, beyond what pure testing can achieve. This confidence is brought about, essentially, by analysis in terms of mathematics and logics. In the course we study some important tools and techniques that have been developed for this purpose, their foundations (i.e. how and why they work), and their applications to some concrete case studies (protocols and programs). Part of the message we want to get across is that formal methods can be actually really useful. During the course students will get exposed to three main approaches in the formal methods area, namely: Hoare logic and weakest precondition calculus, process algebra and process equivalences, and temporal logic model checking.

The course is given in English. However, students can use Swedish when writing reports and exams, and when communicating with the lecturer.

Staff

Course leader and lecturer: Dilian Gurov, e-mail dilian at csc.kth.se, phone 08-790 81 98.

Visiting address: Osquars backe 2, floor 4, room 4417.