Course Catalog 2010-2011 International Basic Pori International Postgraduate Open University |Degrees|     |Study blocks|     |Courses|

Course Catalog 2010-2011

OHJ-2506 Program Verification, 5 cr

Person responsible

Antero Kangas, Antti Valmari

Lessons

Study type	P1	P2	P3	P4	Summer	Implementations	Lecture times and places
Lectures Excercises	4 h/week  2 h/week	+3 h/week +3 h/week				OHJ-2506 2010-01	Tuesday 12 - 14, TC 210 Thursday 12 - 14, TC 128

Requirements

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

Principles and baselines related to teaching and learning

-

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

Evaluation criteria for the course

Exercises and exam.

Assessment scale:

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

Partial passing:

Completion parts must belong to the same implementation

Prerequisites

Course	Mandatory/Advisable	Description
OHJ-2100 Basic Tools for Software Science	Mandatory

Prerequisite relations (Requires logging in to POP)

Correspondence of content

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

Additional information

Suitable for postgraduate studies

More precise information per implementation

Implementation	Description	Methods of instruction	Implementation
OHJ-2506 2010-01

Last modified

20.08.2010