Skip to content
Research Fellows Directory

Martin Ward

Dr Martin Ward

Research Fellow


De Montfort University

Research summary

Suppose you have a computer program and you want to show that it works.

You could run it and see if you get the right answer.

But that only shows that it works for that particular input data.

There are a huge number of different values of input:

far to many to test all of them.

Instead of (or as well as) testing, you can use mathematical

logic to prove, or deduce, properties of the program.

Mathematics can prove things about an infinite set of data: for example,

we can prove that there are an infinite number of prime numbers.

Using mathematical logic we can prove that a program

is correct for ALL possible input data.

Mathematical logic has been around for centuries, but in the 1960's,

Carol Karp developed methods for extending logic so that you

can use infinitely long formulae. With this "infinitary logic"

we can write formulae about loops in programs: the formulae

are infinitely long, because we don't know exactly how many times

the program will go around the loop.

A "program transformation" is any operation on a program which

generates a new program which is equivalent to the original.

So the transformed program produces the same output as the original

program, when it is given the same input.

My research into program transformations started as a piece of pure

"blue skies" research with no commercial application. This research

turned out to have practical applications in reverse engineering:

this is analysing a program in a low-level language to determine

what it does and to translate it into a higher level language.

Many large organisations have systems running on mainframe computers:

which are very expensive to operate and maintain. My research

enables these companies to move some or all of their systems onto

more cost-effective PCs or workstations in a form which is much

easier to maintain.

A commercial company, Software Migrations Ltd, was set up to exploit

this research and now carries out migration projects involving millions

of lines of code.

Grants awarded

An industrial strength software reengineering approach

Scheme: Industry Fellowship

Dates: Nov 2009 - Oct 2013

Value: £98,006