Institute of Computer Languages

Compilers and Languages Group

# Talks 2009 - Nikolaj Popov

The Compilers and Languages Group invites you to a talk given by

### Dr. Nikolaj Popov

RISC-Linz, Johannes Kepler University, Linz, Austria

on

### Specification, Verification and Synthesis of Tail Recursive Programs in Theorema

Date: |
Wednesday, February 5th, 2009 |

Time: |
10:00 (c.t.) |

Location: |
TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte) |

#### Abstract:

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 developed in our PhD thesis.

(This is joint work with Tudor Jebelean.)

#### About Dr. Nikolaj Popov
:

Nikolaj Popov is a postdoctoral researcher
in the Theorema group of Prof. Bruno Buchberger and Prof. Tudor
Jebelean, at the Research Institute for Symbolic Computation,
University of Linz, Austria.

His research deals with the development of a relevant theory for
proving correctness of recursive programs in an automatic manner. His
particular focus is on the automatic generation of a necessary and
sufficient set of verification conditions in order for the program to
be correct.

He holds an MSc from Sofia University, Bulgaria, and a PhD degree from
the Research Institute for Symbolic Computation of the Johannes Kepler
University, Linz, Austria.
(http://www.risc.uni-linz.ac.at/home/npopov)

Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine
druckfertige Einladung im pdf-Format dafür finden Sie
hier.