|
|
|||||||||||||||||
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 |