Data on the course

Show instruction and examinations
814660S Program Correctness, 5 ECTS cr 
Code 814660S  Validity 01.08.2011 - 31.10.2012
Name Program Correctness  Abbreviation Program Correct 
Scope5 ECTS cr   
TypeAdvanced Studies Discipline3259 Information Processing Science 
  Grading1 - 5, pass, fail 

Antti Siirtola 

ECTS Credits 

5 ECTS credits/134 hours of work

Language of instruction 



1 st – 2 nd year of Master’s studies, autumn semester, period 1


Learning outcomes 

After completing the course, the student can list and classify methods and tools available for formal verification. She/he can compare the strengths and limitations of the approaches of a different kind and is able to choose a suitable method for a verification task at hand. More specifically, the student is capable of formulating specifications in propositional, predicate and temporal logic and modelling systems in predicate logic and as finite-state machines. She/he can apply model checking in the analysis of concurrent systems and invent invariants and use proof calculus to establish the (partial) correctness of sequential algorithms.



1. Propositional logic;

2. Predicate logic;

3. Micro models of software;

4. Temporal logic;

5. Model checking;

6. Partial and total correctness;,

7. Proof rules for program correctness;,

8. Programming by contract.


Mode of delivery 

Face-to-face teaching


Learning activities and teaching methods 

Lectures 32 hours, exercises 24 hours, autonomous work 78 hours

Target group 


Prerequisites and co-requisites 

The successful completion of the course necessitates programming skills and the basics of logic and graph algorithms. In terms of courses, it means introduction to programming, discrete structures, data structures and algorithms.

Recommended optional programme components 


Recommended or required reading 

1. Text book: Michael Huth, Mark Ryan: Logic in Computer Science. Modelling and Reasoning about Systems (Chapters 1-4). Cambridge University Press, 2004, 2. lecture material, 3. exercise material.

Assessment methods and criteria 

By taking either three partial exams or a single final exam




Person responsible 

Antti Siirtola

Working life cooperation 



Current and future instruction
No instruction in WebOodi

Future examinations
No examinations in WebOodi