| EPSRC Reference: |
EP/D034906/1 |
| Title: |
Modular Abstraction and Abstraction Refinement: A Game-Semantic Approach |
| Principal Investigator: |
Ghica, Professor DR |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Birmingham |
| Scheme: |
First Grant Scheme Pre-FEC |
| Starts: |
01 March 2006 |
Ends: |
30 November 2008 |
Value (£): |
128,758
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Computer programs often have errors. Detecting errors in computer programs has always been a central problem of computer science. In recent years a technique called 'model checking' was developed in order to find such errors automatically. This technique applies best to programs that are small and comparatively simple. To verify larger programs we need to break them up into smaller parts called sub-programs. Unfortunately, the technique of model checking does not work well for sub-programs, but only for whole programs. In other words, it is not 'modular.'We propose to enhance software model checking using the theory of 'game semantics,' a new theory that provides precise mathematical models for computer programs. The models are modular, so they work for sub-programs, therefore can be used to verify large programs.The techniques used in model checking cannot be used to handle the models provided by game semantics. Our main objective is to adapt these techniques to game semantics, as well as to invent new techniques suitable to game semantics. If our project is successful we should be able to develop an enhanced ability to verify larger programs in a modular way.
|
|
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.bham.ac.uk |