One of the major challenges in computer science is
to put programming on a firmer mathematical basis,
in order to improve the correctness of programs.
This book presents a semantic framework for
verifying safety properties of open sequential
programs. The presentation is focused on an Algol-
like language that embodies many of the core
ingredients of imperative and functional languages
and incorporates data abstraction in its syntax.
Game semantics is used to obtain a compositional,
incremental way of generating accurate models of
programs. Model-checking is made possible by giving...