|
OHJ-2506 Program Verification, 5 cr |
Antero Kangas, Antti Valmari
Lecture times and places | Target group recommended to | |
Implementation 1 |
Periods 3 3 - 4 |
Exercises, exam (or just exercises).
Completion parts must belong to the same implementation
-
Ability to verify parts of programs, algorithms and data structures using logic and set theory. Formal methods' fundamental and practical limitations.
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 |
Exercises and exam.
Numerical evaluation scale (1-5) will be used on the course
Course | Mandatory/Advisable | Description |
MAT-20600 Discrete Mathematics | Mandatory | |
OHJ-2100 Basic Tools for Software Science | Mandatory |
Course | Corresponds course | Description |
|
|
Description | Methods of instruction | Implementation | |
Implementation 1 |