Towards Automation of Algorithm Validation
Dr. Nikolaj PopovDec. 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 ﬁrst-order predicate logic formulae – veriﬁcation conditions. As a distinctive feature of our method, these formulae are not only suﬃcient, 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 speciﬁcation 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.