|
The Program Transformation and Analysis Group's work is
concerned with theoretical aspects of static program analysis.
We are investigating a variety of
partial semantic preserving program simplification methods
primarily using techniques associated with slicing.
The projects we are involved in include:
- Conventional Slicing
- We have produced a new algorithm for slicing unstructured programs
[5] and also
have implemented a number of novel slicing algorithms.
These include, Espresso [2]
a concurrent implementation of Weiser's algorithm in multi-threaded Java.
- Amorphous Slicing
- Amorphous slicing simplifies a program while preserving a
projection of its semantics.
Unlike conventional slicing,
in amorphous slicing all semantics preserving
transformations are allowed.
As well as having produced the first implementation of an
amorphous program slicer based on the system dependence graph
[], we have also developed a theoretical
framework of program projection upon which amorphous slicing
is based [4,6,12].
- Conditioned Slicing
- Conditioned slicing is a powerful generalisation of
static and dynamic slicing with applications in many areas
of software maintenance including re-use and program
comprehension.
Algorithms for implementing conditioned slicing involve
reasoning about the values of program predicates in certain
sets of states derived from the conditioned slicing algorithm,
making implementation particularly demanding.
We have produced a conditioned silcing system called ConSIT [1,3] which is based upon static, slicing, symbolic execution
and theorem proving.
ConSIT is the the first fully automated implementation of
conditioned slicing.
- Theory of Program Schemas
- A program schema defines a class of programs, all of which have identical statement structure,
but whose expressions may differ.
We have introduced the concept of linear schemas, closely related to Control Flow Graphs,
and proved that given any two structured schemas which are conservative, linear and free, it is
decidable whether they are equivalent []. We are currently
working on other results regarding decidability of linear
schemas.
- Program Slicing to Assist Testing
- We have shown how slicing can be used to help program testing
[9,10] and in software
metrics [8].
While mutation testing has proved to be an effective way of finding
faults, currently it is only applied to relatively small
programs. One of the main reasons for this is the large amount of human
analysis required in detecting equivalent mutants. We use
program slicing to reduce the number of equivalent
mutants produced [11,7].
- See
VASTT
for further details.
Members of this group include:
|