My Research
![[Ariane 5]](http://www.comp.leeds.ac.uk/hill/images/ariane5.jpg)
|
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
- verify properties of the software,
- help debug the source program, and
- aid the compiler produce efficient run-time code.
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.