| EPSRC Reference: |
GR/N11667/01 |
| Title: |
INFINITE STATE MODEL CHECKING USING PARTIAL EVALUATION AND ABSTRACT INTERPRETATION |
| Principal Investigator: |
Leuschel, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Electronics and Computer Science |
| Organisation: |
University of Southampton |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 July 2000 |
Ends: |
30 June 2002 |
Value (£): |
52,747
|
| 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 |
|
Infinite model checking is essential for the validation of realistic software, but, by its very undecidable nature, is a daunting task, and no satisfactory solutions exist to that point.This research proposal aims at solving some of the intricate problems encountered during infinite model checking by using technology that has been developed to tackle similar problems in the context of analysis and specialisation of declarative programs: - abstract interpretation, which allows one to approximate an infinite state system by finite one, and ensures that the reasoning performed on the abstraction is valid for the infinite state system.- partial evaluation technology, which will be used to automatically obtain a finite, but still as precise as possible abstraction. Indeed, in program specialisation and partial evaluation, one is faced with infinite computation trees which have to be abstracted in a finite but also as precise as possible way to ensure that non-trivial optimisations can be performed. The problems faced are thus very similar, and the technology developed for partial evaluation might prove to be highly relevant.The potential of this approach will thus be closely investigated.
|
|
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.soton.ac.uk |