Skip to main content

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 their usefulness.

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 values.

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 bytecode.

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

John Gallagher.