Département d'ingénierie informatique

Programming Languages and Systems

Abstract Interpretation

Project leader : B.Le Charlier

Researchers : F. Gobert, I. Polet

Collaborations : Framework : Centre Fédéré en Vérification funded by the FNRS

Funds : FNRS, FSR

Description :

Abstract interpretation is a mathematical methodology (introduced in 1977 by Patrick and Radhia Cousot) to develop static analyses of programs. Such analyses are performed at compile-time or independently of any program execution. They aim at automatically computing semantic properties of the program, which may then be used to optimize compilation or to highlight programming errors. We currently apply abstract interpretation to logic programs (Prolog) and to object-oriented programs (Java). We work on the definition and implementation of generic frameworks to analyze these languages.

A generic abstract interpretation framework has been developped for a subset of Java. This generic framework has been completely implemented and it has been applied to the analysis of typical (moderate-sized) programs. Current and future research activities are concerned with (a) the extension of this generic framework to the whole Java language, (b) the definition of a formal specification language to annotate programs in order to facilitate their verification, (c) the integration of our work to existing software platforms like ECLIPSE and SOOT, (d) the study of new abstract domains allowing one to perform more efficient or more precise analyses.

An analyzer of operational properties of logic programs has been implemented. Its originality is to combine in a single analysis almost all identified analyses from literature: modes, types, variable sharing, determinacy, derivation of the number of solutions to a goal, termination. According to the experiments performed with this analyzer on a significant set of classic examples, new analysis techniques have been set up. The current version of the analyzer gives optimal results for most classic program examples. Future researches will focus on (a) the improvement of type analysis, (b) the use of the derived properties for the optimization of Prolog programs and for their automatic translation into Mercury, (c) the detailed theoretical comparison of the analyzer performance with the techniques found in literature. Christophe Leclère (FUNDP) has studied methods to combine abstract domains in order to perform complex analyses. These methods are used in the analyzer we have developed.