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 
TypeCourse   
  Grading1 - 5, pass, fail 
 
   
Unit  

Teachers
Name
Antti Siirtola 

Description
ECTS Credits 

5 ECTS credits/134 hours of work

 
Language of instruction 

 English

 
Timing 

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.

 

 
Contents 

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

 

 
Grading 

1-5

 
Person responsible 

Antti Siirtola

 
Working life cooperation 

No

 


Current and future instruction
No instruction in WebOodi

Future examinations
No examinations in WebOodi