|
| EPSRC Reference: |
EP/D034906/1 |
| Title: |
Modular Abstraction and Abstraction Refinement: A Game-Semantic Approach |
| Principal Investigator: |
Dr DR Ghica |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Birmingham |
| Scheme: |
First Grant Scheme |
| 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: |
| Panel Date | Panel Name | Outcome |
|
28 Jul 2005
|
Computer Science (Tech) July 05
|
Announced
|
|
|
Summary |
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.
|
| Final Report Summary |
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 enhanced 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 conventional techniques of model checking cannot be used well to handle the models provided by game semantics. We have adapted a number of these techniques (on-the-fly modeling, symbolic modeling, predicate abstraction) to game semantics and we have invented new techniques suitable in particular to game semantics ('clipping'). Based on these theoretical developments we have created a greatly enhanced automated program verification tool called 'Mage' which is freely available online for download.
An unexpected outcome of this research was the development of a new technique ('Geometry of Synthesis') for automated synthesis of digital circuits from 'software' programs, a technique that is rooted in research insights gained from studying programming languages ('Syntactic Control of Concurrency') that are expressive yet can be automatically verified. This development has led to an international patent filing and a 50,000 grant from the Advantage West Midlands agency towards building a prototype tool and investigating commercialization opportunities.
|
| Further Information: |
|
| Organisation Website: |
http://www.bham.ac.uk |
|
|