Modular Abstraction and Abstraction Refinement: A Game-Semantic Approach

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.