MAT-71506 Program Verification, 5 cr

Additional information

Suitable for postgraduate studies

Person responsible

Antero Kangas

Lessons

Implementation 1: MAT-71506 2015-01

Study type P1 P2 P3 P4 Summer

Lectures
Excercises
4 h/week
2 h/week
+3 h/week
+3 h/week

Requirements

Exercises, exam (or just exercises).
Completion parts must belong to the same implementation

Learning Outcomes

Ability to verify parts of programs, algorithms and data structures using logic and set theory. Formal methods' fundamental and practical limitations.

Content

Content Core content Complementary knowledge Specialist knowledge

1. Weakest preconditions

2. Verification techniques for loops

3. Verification of algorithms

4. Analysis and comparison of data structures using set theory

Instructions for students on how to achieve the learning outcomes

Exercises and exam (or just exercises).

Assessment scale:

Numerical evaluation scale (1-5) will be used on the course

Partial passing:

Completion parts must belong to the same implementation

Correspondence of content

Course Corresponds course Description

MAT-71506 Program Verification, 5 cr OHJ-2506 Program Verification, 5 cr

Last modified 10.02.2015

Study type	P1	P2	P3	P4	Summer
Lectures Excercises	4 h/week 2 h/week	+3 h/week +3 h/week

Content	Core content	Complementary knowledge	Specialist knowledge
1.	Weakest preconditions
2.	Verification techniques for loops
3.	Verification of algorithms
4.	Analysis and comparison of data structures using set theory

Course	Corresponds course	Description
MAT-71506 Program Verification, 5 cr	OHJ-2506 Program Verification, 5 cr