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


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)


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

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

   About Us
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)