The project is funded by
EPSRC for
the year 01/02/2005 -- 31/01/2006.
This project concerns the construction of a new range of numerical
domains for static program analysis.
These domains will characterise numerical
properties of computer software such as its computational behavior,
complexity and computed results.
These domains will provide
descriptions for both discrete and
continuous numerical values and relations between them;
operations for extracting the information about these values
from the programs;
primitives for propagating this information forward and/or
backwards;
extrapolation operators that accelerate the convergence of
fixpoint operations;
widening techniques that ensure the convergence of the analysis
and return (approximate) results within the available computing
resources.
The correctness (and hence the safety of any derived
information) of this domain and its related technologies will be proven
using the underlying formal framework of abstract inmterpretation on
which it will be based. By implementing these domains within the
Parma Polyhedra Library (PPL)
which is free software, distributed
under the terms of the GNU Public License, the existing range of
numerical domains in the PPL will be available as candidates for the
continuous component; while a new domain of grids currently being
developed at Leeds will provide an initial basis for candidates for
the discrete component. Using analyzers that already use the PPL to
provide support for a domain of polyhedra
(such as China, a data-flow
analyzer for CLP programs, the
cTI,
a left-termination inference tool
for ISO-Prolog, and the
Action Language Verifier, a verifier of
specifications of reactive software systems), the techniques will be
evaluated in a variety of programming applications.
![[Chiara]](http://www.comp.leeds.ac.uk/hill/images/cooltext3006597.png)