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.