Madalina Erascu

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

VCLA will be hosting a talk by Madalina Erascu on November 20th, 2012.

DATE:Tuesday, November 20, 2012
VENUE:Seminar room Menger (Favoritenstrasse 9-11, 3rd floor)


In this talk we present logical and algebraic approaches for analyzing imperative recursive algorithms and for synthesizing optimal algorithms. First we develop, formalize, and prove automatically, in the Theorema system (, the soundness of a method for the veri cation 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 veri cation. 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 de finition, in the object theory, of the function implemented by the program. Termination, defi ned 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 epsilon", fi nd a real interval such that it contains sqrt(x) and its width is less than epsilon. We use iterative refi ning as algorithm schema: the algorithm starts with an initial interval and repeatedly updates it by applying a refi nement map, say f, on it until it becomes narrow enough. Then the synthesis amounts to fi nding a refine ment map f that ensures that the algorithm is correct (loop invariant), terminating (contraction), and optimal. All these could be formulated as quantifi er 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 quanti er 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).

Comments are closed.