Computational Logic and Quantifier Elimination Techniques for (Semi-)automatic Static Analysis and Synthesis of Algorithms

Madalina Erascu

5 March 2014, 12 March 2014

In this talk we present logical and algebraic approaches for analyzing imperative recursive algorithms and for synthesizing optimal numerical algorithms.

First, we develop, formalize, and prove automatically, in the Theorema system (www.theorema.org), the soundness of a method for the verification of imperative recursive programs. Our goal is to identify the minimal logical apparatus necessary for formulating and proving (in computer-assisted manner) a correct collection of methods for program verification. Our work shows that reasoning about programs does not necessarily need a complex theoretical construction, because it is possible to transfer the semantics of the program into the semantics of logical formulas, thus avoiding any special theory related to program execution. We express the semantics as an implicit definition, in the object theory, of the function implemented by the program. Termination, defined also in the object theory, is an induction principle developed from the structure of the program with respect to iterative structures (recursive calls and while loops). An object theory is the theory relevant to the predicates, constants, and functions occurring in the program text. Currently, our method can be applied to programs with single recursion and with arbitrarily-nested loops with abrupt termination (break, return).

Second, we investigate methods for synthesizing optimal algorithms. As a case study, we consider the square root problem: given the real number x and the error bound e, find a real interval such that it contains sqrt(x) and its width is less than e. We use iterative refining as algorithm schema: the algorithm starts with an initial interval and repeatedly updates it by applying a refinement map, say R on it until it becomes narrow enough. Then the synthesis amounts to finding a refinement map R that ensures that the algorithm is correct (loop invariant), terminating (contraction), and optimal. All these could be formulated as quantifier elimination over the real numbers. Hence, in principle, they could be performed automatically. However, the computational requirement is huge, making the automatic synthesis practically impossible with the current general quantifier elimination software. Therefore, we performed some hand derivations and were able to synthesize semi-automatically optimal algorithms under natural assumptions.

This is joint work with Tudor Jebelean (RISC, Austria) and Hoon Hong (NCSU, USA).