| EPSRC Reference: |
GR/S52759/01 |
| Title: |
Scalable Software Model Checking Based on Game Semantics |
| Principal Investigator: |
Lazic, Professor R |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Warwick |
| Scheme: |
First Grant Scheme Pre-FEC |
| Starts: |
01 November 2003 |
Ends: |
31 October 2006 |
Value (£): |
73,372
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Model checking has been a highly successful approach to verification of hardware and protocols. Recently, model checking of software has become an active and important area of research and application. In contrast to hardware and protocols, software is often highly structured, and contains objects, higher-order computation, complex control mechanisms, pointers, concurrency, and other features. Although impressive tools have been built, a number of substantial challenges remain for software model checking.One of the main breakthroughs in theoretical computer science in the past decade has been the development of game semantics, which has produced the first accurate models for a variety of programming languages and logical systems. Founding software model checking on game semantics has the potential to overcome most of the remaining challenges, because the models are compositional in the style of denotational semantics, yet have clear operational content.We propose contributions to theory and practice of the novel research direction of software model checking based on game semantics. Our main goal is to enable compositional verification of programs and specifications which contain large, polymorphic or infinite data types. This has not been addressed so far, but is necessary for the approach to scale to industrial software.
|
|
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.warwick.ac.uk |