Program Analysis & Logic Programming

My Research

[Ariane 5] The failure of the Ariane 501 was caused by the complete loss of guidance and altitude information ... This loss of information was due to specification and design errors in the software .... The internal SRI [Inertial Reference System] software exception was caused during execution of a data conversion .... The floating point number which was converted had a value greater than what could be represented by a 16-bit signed integer.

Unreliability in software is costly in time and money for all users, can cause expensive equipment failure and, on occasions, lead to fatalities. Therefore there is an increasing demand for more robust software with guaranteed performance. (Evidenced by the fact that Microsoft now has top-level research teams actively working on static program analysis; SLAM). More specifically there is a need for reliable tools that can My research aims to provide such tools and techniques needed to help satisfy this demand.

The design and methodology used for the analysis tools is based on Abstract Interpretation (AI) which has successfully been used for constructing algorithms to statically determine run-time properties of programs. The key notion is to approximate the program's semantics by defining an abstract domain with operations which mimic those of the concrete domain. Central to AI is the choice of abstract domain used to describe relevant program properties. Since most domains that simply represent an interesting property lose too much information in the abstract interpretation of the program, the results with such domains are normally rather imprecise. In fact, there is an art in finding good domains that provide accurate information within an acceptable period of time and memory. How such domains can be constructed, combined and refined is a major part of the current research.

Logic programming (LP) is one of the principal paradigms for declarative reasoning. This separates the specification of what has to be solved from the control information that aids the search for a solution. Thus a logic program can be read as a set of logical formulas which can also be executed as a computer program. Prolog is the main one of many programming languages based on this formalism. The application of program analysis to Prolog has been particularly productive as LP has such a well-defined semantics, both from the declarative and from the procedural perspectives.