Modular Abstraction and Abstraction Refinement: A Game-Semantic Approach
Lead Research Organisation:
University of Birmingham
Department Name: School of Computer Science
Abstract
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.
Organisations
People |
ORCID iD |
Dan Ghica (Principal Investigator) |
Publications
Dimovski A
(2006)
Model Checking Software
Bakewell A
(2008)
Tools and Algorithms for the Construction and Analysis of Systems
Ghica D
(2007)
Geometry of synthesis
Ghica D
(2006)
Syntactic control of concurrency
in Theoretical Computer Science
Ghica D
(2008)
Angelic semantics of fine-grained concurrency
in Annals of Pure and Applied Logic
Description | We have discovered that game semantics can be used to model and verify software compositionally, that is certain properties of the whole program can be determined by examining parts of the program. |
Exploitation Route | Our verification tools and theories can be expanded on in terms of performance and features. In fact a research group in Oxford led by Prof. Ong has done just that. |
Sectors | Digital/Communication/Information Technologies (including Software) |
Description | Several experimental automated verification tools based on game semantics have been developed. This had influence on the work of the "higher-order model checking" group in Oxford, led by Prof. Ong. The work was theoretical and foundational so the impact is only academic. |