| EPSRC Reference: |
GR/M32900/01 |
| Title: |
EXPLOITING DATA INDEPENDENCE |
| Principal Investigator: |
Roscoe, Professor A |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Oxford |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 September 1999 |
Ends: |
28 February 2003 |
Value (£): |
180,345
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| Information Technologies |
No relevance to Underpinning Sectors |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
A program is 'data independent' in type variable T when it makes sense whatever nonempty type is used for T. Over the past few years researchers have developed methods by which model checkers can prove properties of data independent programs for all T. The Investigators have developed this theory for CSP, covering an exceptionally wide range of language constructs and types of program. Their work is beginning to find applications in MOD and industry, and also in academic work on computer security. Tools will soon be under development to support these. This proposal extends the resources available for the development of this theory, in particular by addressing issues that arise from applications and tool developers. The methods used include logical relations, symbolic operational semantics (plus the theory of labelled transition systems including explicit data variables) and symmetry elimination. We will look at other approaches to the automated proof of general results, such as induction, especially where there is a relationship with data independence. Many ideas in data independence transfer intuitively from language to language: we will develop methods, probably by using symbolic operational semantics as a bridge, enabling results to be transferred at a formal level.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.ox.ac.uk |