| |
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.
| |
| 8 | 9 May - 15 May
- Nikolaj Popov: Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs
We describe an innovative method for proving total correctness of tail
recursive
programs having a specific structure, namely programs in which an
auxiliary tail recursive
function is driven by a main nonrecursive function, and only the
specification of the main
function is provided. The specification of the auxiliary function is
obtained almost fully
automatically by solving coupled linear recursive sequences with
constant coefficients.
The process is carried out by means of CA (Computer Algebra) and AC
(Algorithmic
Combinatorics). We demonstrate this method on an example involving
polynomial expressions.
Furthermore, we develop a method for synthesis of recursive programs for
computing
polynomial expressions of a fixed degree by means of "cheap" operations
e.g., additions,
subtractions and multiplications. For a given polynomial expression, we
define its recursive
program in a schemewise manner.
The correctness of the synthesized programs follows from the general
correctness of the
synthesis method, which is proven once for all, using the verification
method presented in
the first part of this talk.
| 
|
