Game semantics is a way of giving meanings to programming languages
(and to logical systems) using basic and intuitive notions of game
playing. The approach goes back to Kleene and Gandy in one tradition,
and to Kahn and Plotkin, and Berry and Curien in another. Compared to
other semantics of programming languages, a striking feature of game
semantics is that it is denotational (and so admits compositional
methods) and yet has clear operational content; further it gives rise
to accurate (fully abstract) models for a wide range of programming
languages. A recent development in game semantics is concerned with
the algorithmic representation of fully abstract game semantics, with
a view to applications in software model checking and program
analysis. The goal is to build on the tools and methods which have
been developed in the Verification community, while exploring the
advantages offered by our semantics-based approach. This talk gives a
survey of recent results in this direction, and discusses a number of
directions for further work.
