The overall aim of Geoff Hamilton's 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 Dr. Hamilton's belief that this will only gain acceptance within industry if it can be automated to the greatest possible extent. His research has, therefore, concentrated on developing automatic techniques for the analysis, transformation and construction of programs.

Dr. Hamilton has developed a number of static analyses of programs to determine their properties automatically, and then shown how this information can be used to optimise these programs. He has also developed a number of automatic transformation algorithms which can be used to transform programs into equivalent programs which run more efficiently.

The current emphasis of Dr. Hamilton's 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, the transformation algorithms which Dr. Hamilton has previously developed can be applied to them to improve their efficiency. The domains within which he has applied the techniques which he has developed include telephone systems and security protocols.