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 [2].
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 [3].
A specialized strategy for proving termination of recursive
functional programs is developed [5]. 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 [4].
Our work is performed in the frame of the Theorema system
[1], 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.).
| [1] | B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa, F. Piroi, N. Popov, J. Robu, M. Rosenkranz, and W. Windsteiger. Theorema: Towards Computer-Aided Mathematical Theory Exploration. Journal of Applied Logic, 2005. | |
| [2] | T. Jebelean, L. Kovacs, and N. Popov. Experimental Program Verification in the Theorema System. Int. Journal on Software Tools for Technology Transfer (STTT), 2008. To appear. | |
| [3] | N. Popov and T. Jebelean. A Prototype Environment for Verification of Recursive Programs. In Z.~Istenes, editor, Proceedings of FORMED'08, pages 121-130, March 2008. To appear as ENTCS volume, Elsevier. | |
| [4] | N. Popov and T. Jebelean. Verification of Functional Programs Containing Nested Recursion. In B. Buchberger, T. Ida and T. Kutsia, editors, Proceedings of SCSS'08, pages 163-175, Hagenberg, Austria, July 2008. | |
| [5] | N. Popov and T. Jebelean. Proving Termination of Recursive Programs by Matching Against Simplified Program Versions and Construction of Specialized Libraries in Theorema. In D. Hofbauer and A. Serebrenik, editors, Proceedings of 9th International Workshop on Termination (WST'07), pages 48-52, Paris, France, June 2007. |
Tudor Jebelean is an Associate Professor in the Theorema group (leader: Bruno Buchberger and Tudor Jebelean) at the Research Institute for Symbolic Computation (RISC), Johannes Kepler University of Linz, Austria. His main research interests are automated reasoning and program verification using logic and algebraic methods. He holds a PhD in Computer Science and Habilitation title from Johannes Kepler University of Linz.
Contact Nikolaj and Tudor at:
Dr. Nikolaj Popov
Research Institute for Symbolic Computation (RISC)
Johannes Kepler University of Linz
A-4040 Linz, Austria
popov at risc.uni-linz.ac.at
http://www.risc.uni-linz.ac.at/home/npopov/
Prof. Dr. Tudor Jebelean
Research Institute for Symbolic Computation (RISC)
Johannes Kepler University of Linz
A-4040 Linz, Austria
Tudor.Jebelean at risc.uni-linz.ac.at
http://www.risc.uni-linz.ac.at/home/tjebelea/