Centre for Metacomputation

During 2006-09 this project, funded by a £431K EPSRC Platform Grant, brought together three research themes at Oxford for a focussed research effort on metacomputation - the study of software programs that operate on other programs. The principal investigators were Samson Abramsky and Luke Ong (foundations), Tom Melham (automated verification) and Oege De Moor (tools). 

Metacomputation covers several fields, including logic, automated theorem proving, compiler construction, program analysis, and software engineering. The Centre set out to integrate some of these separate strands, to develop metacomputation as a field, and to provide it with solid theoretical foundations. Our approach was to conduct a programme of pilot case studies that cut across the research of the individual investigators and lead to further funding proposals. Our aims were to develop

• scalable bug detection at compile-time
• language features for system monitoring
• combinations of multiple hardware verification techniques
• automated support for software renovation

and to investigate the interplay between these applications and foundations.

Among the outcomes were to EPSRC grants for projects on Aspect Refactoring Tools (£546K) and Abstraction Discovery and Refinement for Model Checking Partially Ordered State Spaces (£175K). Scientific outcomes include the first fully abstract model for a functional language of additive aspects, arising from a study of aspect calculi semantics.