Invited Talk

Model checking concurrent programs using game semantics

Dan Ghica

University of Birmingham


The extraction of accurate finite-state models of higher-order or open programs is a difficult problem. We show how it can be addressed using newly developed game-semantic techniques and illustrate the solution with a model-checking tool based on such techniques. The approach has several important advantages over more traditional ones: precise account of inter-procedural behaviour, concise procedure summaries and surprising compactness of the extracted models. Last updated: May 23, 2005