Competency Leader

Geoff Hamilton

The overall aim of this area 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 this will only gain acceptance within industry if it can be automated to the greatest possible extent.

The main focus in this area is therefore on fully automatic techniques for code generation. The major achievement by Lero researchers in this area is the development of the distillation program transformation algorithm. Distillation is a source-to-source transformation algorithm which can be applied to higher-order functional programs to remove intermediate data structures. Distillation represents a major advance over previously existing fully automatic program transformation algorithms. Using previous algorithms it is only possible to obtain a linear improvement in the performance of programs; with distillation a super-linear improvement can be obtained. The simplified form of program which is produced by distillation is also particularly amenable to analysis. It has already been shown how distillation can be used in the verification of safety and liveness properties of programs, and it has also been used in the implementation of the theorem prover Poitín. It has also recently been discovered that the simplified form of program produced by distillation is particularly amenable to parallelisation. Work is ongoing in this area on identifying potential parallelism within programs, and on mapping this potential parallelism to different parallel architectures.

Competency Team

Chris Exton	David Gregg	Geoff Hamilton	Mike Hinchey	Joseph Morris
John Murphy	Mel OCinneide