|
In collaboration with
Roberto Bagnara and
Enea Zaffanella,
this project concerns the ongoing development of the
Parma Polyhedra Library (PPL).
The Parma Polyhedra Library (PPL) is a modern C++ library for
the manipulation of convex polyhedra and other numerical abstractions
being developed by Roberto Bagnara and Enea Zaffanella in Parma and by Dr
Hill at Leeds. This library is: user friendly; fully dynamic; portable;
exception-safe; efficient; thoroughly documented;
and free software distributed under the terms of the GNU General
Public License.
|
Product Domains for Software Analysis
This project
concerns the design and implementation in the
PPL of a
generic product domain that is parameterised not only on
the component domains but also on the reduction that is performed
between the domains.
We are particularly interested in the case when one component domain
is a polyhedron domain (such as the closed convex polyhedron and
octagon domains) and the other is a Grid domain (see below).
We currently support light-weight reduction methods such as that
of sharing equalities as these are not only very efficient
but also are safe to use with standard polyhedral widenings.
Further research is needed to find more precise reduction methods
but with good performance cost
and for which suitable widenings can be constructed.
|
|
This project, partly funded by EPSRC,
concerns the design and implementation in the
PPL of the grid domain;
this is a domain for use in capturing information about the
possible distributions of the numerical values in a program.
Further work is needed in designing and building abstract operations
that approximate the behaviour of the various arithmetic operations
supported by programming languages such as C.
For some non-linear operations, this may lead to the development of
new abstract domains and/or abstract operations.
|
|
The research focuses on a generic imperative language
for which languages such as C and C++
may be considered to be instances. After
specifying the language and its natural semantics, we have
provided a generic abstract semantics that can be combined with
a wide range of abstract domains and proved its soundness
with respect to the natural semantics.
We are now using this specification to build a experimental analyzer
for C programs.
|
|
The research which is in collaboration with
Fausto Spoto
focuses on analyzing interesting properties of
object-oriented languages, particularly Java.
|
|
The project aims to develop improved methods, based on abstract
interpretation, for detecting numerical instability in software caused
by the approximate binary or floating point representations of
numbers.
|
![[Convex Polyhedra]](http://www.comp.leeds.ac.uk/hill/images/abstractions_polys.gif)
![[Rational Grid]](http://www.comp.leeds.ac.uk/hill/images/abstractions_rcongrs.gif)
![[Grid-Polyhedra]](http://www.comp.leeds.ac.uk/hill/images/abstractions_zpolys2.gif)
![[Grid-Polyhedra]](http://www.comp.leeds.ac.uk/hill/images/abstractions_tcongrs.gif)