Introduction
- Theory of Program Schemas
-
Program schemas
define a class of programs, all of which
have identical statement structure, but whose expressions may differ.
Program Schemas have a well developed theory. We have
introduced linear schemas and recently proved that given any two structured schemas which are
conservative, linear and free, it is decidable whether they are equivalent.
Problems that are expressed in terms of a Control Flow Graph
can naturally expressed in terms of Linear Schemas
whose theory can be used to verify the
decidability of solutions to these problems.
We are currently working on other results applying the theory
of linear schemas to program slicing.
- Program Slicing
-
Conventionally, Program
Slicing
simplifies a program, by deleting statements, while preserving a
projection of its semantics.
Currently, we are investigating the existence of minimal slicing
algorithms.
We have introduced Amorphous Slicing
Unlike conventional slicing,
in amorphous slicing all semantics preserving
transformations are allowed.
We have also developed a theoretical
framework of program projection upon which amorphous slicing
is based.
We are investigating problems with slicing
programs with side effects.
We
have implemented a number of novel slicing algorithms.
- Conditioned Slicing using Theorem Provers
-
Program conditioning
involves attempting to simplify a program
assuming that
the states it reaches at various points in its execution satisfy
certain properties. These properties are specified by adding assertions at arbitrary points in the program.
Program conditioning relies upon both symbolic execution
and reasoning about symbolic predicates and therefore requires some form of automated
theorem proving.
We have developed systems that perform program conditioning
with the aid of theorem provers
These are the first fully automated implementations of
program conditioning.
We are also developing
a semantic theory of program conditioning.
- Evolutionary Mutation Testing
-
Mutation Testing involves running slightly
corrupted versions (mutants) of your target program through your
test suite to see if any test cases flag the variations as defects.
This enables us to measure abilty of the test suite to detect bugs.
We are developing methods using genetic algorithms where the mutant programs
and the test suite co-evolve to form a stronger test suite.
