Towards Automation of Algorithm Validation

Dr. Nikolaj Popov

Dec. 9, 2008, 2:30 p.m. MZ 005A

We present some novel ideas for proving total correctness of recursive functional programs and we discuss how they may be used for algorithm validation. As usual, correctness (validation) 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 the Neville’s algorithm for polynomial interpolation and show how it may be validated 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.

This talk is addressed to mathematicians (also physicists and engineers) who are inventing algorithms for solving concrete problems. On one hand, the help comes with the automatically obtained correctness proof. On the other hand, the inventor may try to prove the correctness of any conjecture, and in case of a failure obtain a counterexample, which may eventually help making a new conjecture.