Institute of Computer Languages
Compilers and Languages Group
on
| 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.)
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.