The overall aim of my research is to develop techniques to facilitate the construction of software that is provably correct and efficient, and to apply these techniques to real problems. The use of formal approaches is essential to this, but it is my belief that this will only gain acceptance within industry if it can be automated to the greatest possible extent. My research has therefore concentrated on developing automatic techniques for the analysis, transformation and construction of programs.

The current emphasis of my research is on automatic inductive theorem proving, and the extraction of programs from the resulting proofs. By extracting programs from these proofs in this way, they are guaranteed to meet their logical specifications. As programs which are extracted in this way can be quite inefficient, transformation algorithms can be applied to them to improve their efficiency.

Current Research Students

Humayun Kabir

Biren Patnaik

Previous Research Students

Ben Aziz

Bernadette Power