| EPSRC Reference: |
GR/R27105/01 |
| Title: |
Fully Expansive Proof and Algorithmic Verification |
| Principal Investigator: |
Gordon, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science and Technology |
| Organisation: |
University of Cambridge |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 October 2001 |
Ends: |
30 September 2004 |
Value (£): |
249,299
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The main goal is to develop and test theoretical and methodological concepts to extend fully-expansive (LCF-style) theorem proving to support Automatic verification (including model checking) and efficient execution.A key idea is to devise caluculi of judgements that link logic terms to efficient data structures (like BDDs and MDGs) and then to implement calculations vith these structures as fully-expansive proof in the calculi.\n existing fully-expansive ground execution mechanism will be extended to support symbolic execution. Links will also be provided to program execution mechanisms in the metalanguage that are not fully expansive.,kthe research will emphasise conceptual coherence as well as implementation efficiency. It will build on successful proof-of-concept experiments and :)e tested on public domain models of ARM processors being developed at the University of Leeds.
|
|
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.cam.ac.uk |