A games-based foundation for compositional software model checking

We present a program specification language for Idealized ALGOL that is compatible both with inferential reasoning and model checking. Model-checking is made possible by the use of an algorithmic, game semantic model of the programming language. Inferential reasoning is carried out using rules based on Hoare's logic of imperative programming, extended to handle procedures and computational side effects. The main logical innovation of this approach is the use of generalized universal quantifiers to specify properties of non-local objects. Together, the regular-language semantics of the programming language and its specification language on the one hand, and the inferential properties of the specification language on the other provide a foundation for compositional software model checking.