|
|
|||||||||||||||||
Course Catalog 2012-2013
OHJ-2506 Program Verification, 5 cr |
Additional information
Suitable for postgraduate studies
Person responsible
Antero Kangas, Antti Valmari
Lessons
| Study type | P1 | P2 | P3 | P4 | Summer | Implementations | Lecture times and places |
|
|
|
|
|
|
|
|
|
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:
Prerequisites
| Course | Mandatory/Advisable | Description |
| OHJ-2100 Ohjelmistotieteen perustyökaluja | Mandatory |
Prerequisite relations (Requires logging in to POP)
Correspondence of content
| Course | Corresponds course | Description |
|
|
|
|
|
|
|
More precise information per implementation
| Implementation | Description | Methods of instruction | Implementation |