| |
Time: Wednesday, 12:30-14:00 .
Room: HA 105 (Hagenberg seminar room).
Start: March 21, 2006.
In this seminar, we explore current research
and systems for specifying and verifying computer programs
(specification languages, program verifiers, model checkers, ...). This
continues the seminar of the previous semester.
To take part in the seminar, you have to enrol in the KUSSS system. If you also login in Moodle and register as a course participant, you will receive per email all
messages posted in the News forum.
| |
| 6 | 25 April - 1 May
- Nikolaj Popov: Logical Aspects of Algorithm Verification
We present a method for proving total correctness of recursive
programs having multiple recursive calls by obtaining verification
conditions. The method itself is not only sound but also complete,
that is, the verification conditions are necessary and sufficient
conditions for the total correctness. Special emphasis is put on the practical applicability of the completeness, especially how it may help debugging. By the end, we demonstrate how correctness of computational methods, in particular Neville's algorithm for polynomial evaluation, may be proven.
| 
|
