Program Analysis with Exact Approximations

Markus Müller-Olm
FernUniversität in Hagen, Germany
Friday, 23 April, 2004 (All day)
Louvain-la-Neuve University (UCL) classroom BARB91

Automatic program analyses that determine run-time properties of programs are needed in optimizing compilers and for validation of programs. Due to fundamental recursion-theoretic reasons, however, all non-trivial semantic properties are undecidable in programs of a computationally-universal programming language. One way out is to work with approximate analyses. Such analyses determine certain but not necessarily all valid properties of a given type; they are correct but in general incomplete ("approximate").

This leads to the question how to assess the precision of an approximate analysis. One way to do so is to define an abstraction of programs and to show that the approximate analysis solves the abstracted problem thus obtained exactly. Abstraction also allows us to study abstracted analyses problems as such. In order to do so we fix a (hopefully natural) abstraction, establish (un-)decidability and complexity results for the abstracted problem, and construct algorithms that solve the abstracted problem completely and as efficient as possible. The talk reports on some results of this kind obtained in recent years in various classes of programs. The goal of such studies is to get a better understanding of the trade-off between efficiency and precision in the construction of approximate analysis algorithms and to uncover potential for construction of better analysis algorithms.