A Toolkit for Program Analysis and Transformation
Program analysis and transformation concerns
optimisation, synthesis, debugging and
verification of program source code. In Bristol,
the main topics being studied
are program specialisation and abstract interpretation.
The aim of the project is to build a suite of tools and demonstrate
Tools for Program Specialisation
Program specialisation tools are being built for
various target languages, including a higher-order
functional and logic language, constraint logic
programming languages, and
imperative languages such as C, Java and bytecode. Specialisation
is an optimisation technique in which
a program is optimised to handle only some of its possible input
Specialisation experiments using the tools have been carried out in the
following domains; proof procedures for predicate logic, with
application to formal verification;
animators of the hardware description
language VERILOG; semantics-based
declarative interpreters for imperative languages such as C, Java and
Tools for Abstract Interpretation
Abstract interpretation is a method of symbolic execution,
which allows all possible behaviours of a program
to be predicted. The set of behaviours is an approximation, in the
sense that some extra behaviour might be included as well
as the actual behaviour of the program.
This provides a way of verifying properties
of interest, since properties which hold in the set of all
predicted states clearly also hold in all actual states.
A set of practical tools is being built on the theoretical framework
of abstract interpretation.
Effort is focussed in the following areas:
development of tools supporting
systematic generation of abstract interpretations for different
languages, by mapping them into constraint logic programs;
precise approximation of constraint logic programs using convex
polyhedra, regular approximations and combinations of these methods.
Staff and Students