Game Semantics and Program Verification

Motivation

Game semantics came to prominence in the 1990s when it was used to construct the first fully abstract models for a wide spectrum of programming languages. It views computation as an exchange of moves between two players, representing respectively the program and its environment. Accordingly, a program is interpreted as a strategy in a game corresponding to its type.

Game semantics can describe faithfully an impressive wealth of type theories, including higher-order types, polymorphism and recursive types, as well as untyped languages related to the lambda calculus. Remarkably, by varying combinatorial conditions regarding the shape of admissible plays one can characterize, in the form of a full abstraction result, numerous programming paradigms, including concurrency, functional programming, imperative programming and higher-order references. This accuracy in modelling makes game semantics stand out from other semantic theories, which lack similar robustness.

The combination of the concrete with the abstract embodied by game models has recently led to the formulation of a research programme, called algorithmic game semantics, that aims to develop the field in a new direction with a view to applications in computer-assisted verification and program analysis. Game semantics offers a radically different approach to modelling program state from the standard approach in the verification literature. For example, it does not model internal execution details such as values of variables or function calls in an explicit way. Instead, the plays it generates correspond to the observable patterns that a program produces when interacting with its environment through its indeterminate components (variables). As a consequence, open programs - an object of much current interest in software verification - can be modelled with the same ease as closed ones, which cannot be said about other treatments in the literature. In the last few years this has led to a series of new results in program verification, in which game semantics has played a crucial role. In particular, its expressiveness and robustness bring the promise of a sound transfer of standard methods applied in verification, such as abstract interpretation and model checking, to more structured programming situations studied by the semantics community.

We believe the time has come for a more systematic assessment of what the two areas have to offer to one another. Thus, critical evaluation of what has been achieved so far and establishing common realistic research goals for the future will be the primary objectives of the proposed seminar, in addition to broadening and deepening the participants' knowledge about the subjects. The format of a Dagstuhl seminar is ideally suited for this, potentially fruitful, cross-fertilization to take place.