TCS / Studies / T-79.5305 Formal Methods
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

T-79.5305 Formal Methods (4 cr) P V

Autumn 2006

The course T-79.5305 replaces the course T-79.157 Formal Description and Verification of Computing Systems.

The topic of this course this year is software model checking and abstraction techniques.

Model checking is a technique to algorithmically verify hardware and software systems. It has been succesfully applied to analyze hardware systems and is currently a part of the development process in many hardware design companies such as Intel and IBM. Compared to hardware systems, model checking software systems poses new challenges due to a larger number and domains of variables involved, dynamic memory allocation, more complex concurrency primitives, and in general larger system sizes. These problems have been tackled in the research literature during the last few years, enabling the analysis of more and more complex software systems.

One of the main techniques applied in software model checking is abstraction. The goal of abstraction is to remove parts of the system that are irrelevant to the verification of the desired property either in an exact or over-approximating way. If over-approximation is used, then the analysis may report false negatives (i.e. bugs that are not real bugs in the system) and the applied abstraction has to be refined in order to remove the false negative. As an example of industrial use of abstraction techniques in software system verification, the Static Driver Verifier tool, developed in the SLAM project at Microsoft, relies on so-called predicate abstraction. The tool has recently been beta-released as part of the Windows Driver Foundation. Other similar projects include e.g. Bandera that develops a tool set for model checking concurrent Java software, and Blast providing a software model checker for C programs.

In this course, we will go through research material concerning different abstraction techniques and other similar techniques. The course is organized in a seminar form.


  • [25 Aug 2006] First lecture Wednesday 13th of September, room TB353.


  • Coordinator: Dr. Tommi Junttila
  • Tutors: Prof. Ilkka Niemelä, Doc. Keijo Heljanko, and Lic.Sc.(Tech.) Heikki Tauriainen
  • Seminar meetings: On Wednesdays from 16.15 onwards in the seminar room TB353. The first meeting will be on Wednesday 13th of September.
  • Prerequisites: Basic knowledge of problem representations and logic (T-79.1001, T-79.3001); parallel and distributed systems (T-79.4301); basic knowledge on programming languages (Java, C, etc.)
  • Requirements for passing the course:
    • Attend the seminars (recommended, not required).
    • Give a seminar presentation. The length of the presentation should be 45-90 minutes.
    • Write a short report (5-8 pages) on your presentation topic. The report shoud review the problem, solution, and techniques in the presentation material and include a small self-made example on applying the solution/techniques. The deadline for delivering the report is the wednesday two weeks after your presentation.
    • Act as an opponent for one other presentation. This includes reading the presentation material, preparing and presenting two questions, and generally being active during the presentation.
  • Course web site:

Schedule (tentative)

Will be further refined soon.

Background material

The following material can be useful.
  • The lecture slides of Parallel and distributed systems
  • Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, 1999. Especially the following chapters:
    • Chapters 2, 3, and 4: modelling, temporal logics, and model checking.
    • Chapters 5 and 6: Binary decision diagrams and symbolic model checking.
    • Chapter 9: Model checking and automata theory.
    • Chapter 10: Partial order methods.

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 29 November 2006.