|
| EPSRC Reference: |
EP/D037085/1 |
| Title: |
Centre for Metacomputation |
| Principal Investigator: |
Professor S Abramsky |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Computing Laboratory |
| Organisation: |
University of Oxford |
| Scheme: |
Platform Grants |
| Starts: |
01 March 2006 |
Ends: |
28 February 2010 |
Value (£): |
431,107
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Modelling and Simulation of IT Systems |
| Software Engineering |
Systems Methodology and Architecture |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
25 Jul 2005
|
ICT Platform Interview Panel
|
Announced
|
|
|
Summary |
Metacomputation concerns the development of sophisticated
computational tools for analysing the behaviour of programs. Such
tools may operate at development time, for example to catch bugs, or
they may operate at run-time, for instance to adapt the program to
changing workloads. Techniques in metacomputation draw from a broad
variety of different fields, including logic, automated theorem
proving, compiler construction, program analysis, and software
engineering. The time is ripe to unify these fragmented efforts in
different communities and to help establish the emerging field of
metacomputation and its foundations. To do so is the primary objective
of this proposal.
Examples abound where synergy between these different techniques has
led to striking practical success. The SLAM project at Microsoft
combines techniques from automated theorem proving (both model
checking and deductive proof) as well as program analysis to locate
many faults in device drivers. The Eclipse refactoring tools,
developed at IBM, use a sophisticated system of type constraints to
correctly implement refactoring transformations such as extract
interface. Intel's Forte framework employs a functional programming
language with reflection and metaprogramming features to get an
effective framework for verification of industrial-scale hardware
designs.
Foundational work in semantics has now reached a point where semantics
can be seen, not simply as a mathematical tool for the analysis of
programs, but as leading directly to computational representations and
algorithmic methods. Model-checking can already be seen as a step in
this direction. However, we see great additional potential in the use
of compositional semantic methods in this context; in particular, in
the analysis of open systems. Semantics endowed with a computational
aspect is inherently metacomputational in nature, and many interesting
new questions and possibilities arise. One the one hand, some new and
very direct applications in program analysis can be envisaged. There
are also some fascinating issues around reflection: can a program be
the computational representation of its own semantics, and can such
reflexivity be useful?
More broadly, we see a growing synergy between the semantics and
program analysis community as greatly to the benefit of both,
providing increased depth and formal rigour in program analysis, and
new challenges and links to computational aspects in semantics.
|
| Final Report Summary |
|
No final report summary is available for this grant.
|
| Further Information: |
|
| Organisation Website: |
http://www.ox.ac.uk |
|
|