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


Functional Program Verification in Theorema.
Recent Achievements and Perspectives

Date: Wednesday, February 4th, 2009
Time: 14:00 (s.t.)
Location: TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte)


We present an environment designed for proving total correctness of recursive functional programs.
As usual, correctness is transformed into a set of first-order predicate logic formulae - verification conditions. As a distinctive feature of our method, these formulae are not only sufficient, but also necessary for the correctness.
We demonstrate our method on several examples and show how correctness of those may be proven fully automatically.
In fact, even if a small part of the specification is missing - in the literature this is often a case - the correctness cannot be proven. Furthermore, a relevant counterexample may be constructed automatically.
A specialized strategy for proving termination of recursive functional programs is developed. The detailed termination proofs may in many cases be skipped, because the termination conditions are reusable and thus collected in specialized libraries. Enlargement of the libraries is possible by proving termination of each candidate, but also by taking new elements directly from existing libraries.
During the talk, we emphasize on the most recent achievements we have made, and in particular verification of functions defined by mutual recursion and functions containing nested recursion.
Our work is performed in the frame of the Theorema system, which is a mathematical computer assistant aiming at supporting all the phases of mathematical activity: construction and exploration of mathematical theories, definition of algorithms for problem solving, as well as experimentation and rigorous verification of them. Moreover, the logical verification conditions can be passed to the automatic provers of the system.
Theorema includes a collection of general as well as specific provers for various interesting domains (e.g., integers, sets, reals, tuples, etc.).
   (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 | Datenschutzerklärung | last update: 2018-05-25 (Webmaster)