Semantics-directed abstraction and refinement

Game semantics provides a new method for extracting finite-state
models from open programs that exhibit non-trivial interactions
between procedures and state. However, the problem of state-space
growth is as acute in the case of game models as is in the case of
models obtained using traditional, operational, methods. Two of the
most successful techniques dealing with this problem are abstract
interpretation and counterexample-guided refinement. I will present
recent advances in applying these ideas within the game-semantic
framework, from foundations to tool implementations.