In recent years, Game semantics has been used with considerable success to give precise (`fully abstract') models for programming languages with rich combinatios of features, including higher-order procedures, locally scoped imperative vasiables, control operators such as call-cc, non-determinism and probabilistic choice.

Current work is now turning in an algorithmic direction, by finding explicit automata-theoretic representations of the game semantics, as a basis for model-checking and program analysis. A particualrly promising feature of this approach to software model-checking is that it is inherently *compositional*: since the semantics applies directly to open programs (with free variables), so does the analysis based on it. Moreover, soundness of the analysis is guaranteed by the foundational work on the semantics on which it is based.

We shall illustrate these ideas by looking at the game semantics for a block-structured procedural language with locally-scoped variables, and showing how this can be developed in algorithmic form.