This paper presents a semantic framework for data abstraction and refinement for verifying safety properties of open programs with integer types. The presentation is focused on an Algol-like programming language that incorporates data abstraction in its type system. We use a fully abstract game semantics in the style of Hyland and Ong and a more intensional version of the model that tracks nondeterminism introduced by abstraction in order to detect false counterexamples. These theoretical developments are incorporated in a new model-checking tool, Mage, which implements efficiently the data-abstraction refinement procedure using symbolic and on-the-fly techniques.

After informally reviewing the main concepts from game semantics and placing the development of the field in a historical context we examine its main applications. We focus in particular on finite state model checking, higher order model checking and more recent developments in hardware design.

In this paper we introduce clipping, a new method of syntactic approximation which is motivated by and works in conjunction with a sound and decidable denotational model for a given programming language. Like slicing, clipping reduces the size of the source code in preparation for automatic verification; but unlike slicing it is an imprecise but computationally inexpensive algorithm which does not require a whole-program analysis. The technique of clipping can be framed into an iterated refinement cycle to arbitrarily im prove its precision. We first present this rather simple idea intuitively with some examples, then work out the technical details in the case of an Algol-lik e programming language and a decidable approximation of its game-semantic model inspired by Hankin and Malacaria's lax functor approach. We conclude by prese nting an experimental model checking tool based on these ideas and some toy programs.

We introduce a technique for using conventional predicate abstraction methods to reduce the state-space of models produced using game semantics. We focus on an expressive procedural language that has both local store and local control, a language which enjoys a simple game-semantic model yet is expressive enough to allow non-trivial examples. Our compositional approach allows the verification of incomplete programs (e.g. libraries) and offers the opportunity for new heuristics for improved efficiency. Game-semantic predicate abstraction can be embedded in an abstraction-refinement cycle in a standard way, resulting in an improved version of our experimental model-checking tool Mage, and we illustrate it with several toy examples.

The problem of synthesis of gate-level descriptions of digital circuits from behavioural specifications written in higher-level programming langu ages has been studied for a long time yet a definitive solution has not been for thcoming. The contribution of this paper is mainly methodological, bringing a perspective that is informed by programming-language theory. We argue that one of the major obstacles in the way of hardware compilation becoming a useful and mature technology is the lack of a well defined function interface model, i.e. a canonical way in which functions communicate with arguments. We discuss the consequences of this problem and propose a solution based on new developments in programming language theory. We conclude by presenting an implementation and examples.

We introduce on-the-fly composition, symbolic modelling and lazy iterated approximation refinement for game-semantic models. We present Mage, an experimental model checker implementing this new technology. We discuss several typical examples and compare Mage with Blast and GameChecker, which are the state-of-the-art tools in on-the-fly software model checking, and game-based model checking.

We introduce a game model for an Algol-like programming language with primitives for parallel composition and synchronization on semaphores. The semantics is based on a simplified version of Hyland-Ong-style games and it emphasizes the intuitive connection between the concurrent nature of games and that of computation. The model is fully abstract for may-equivalence.

We propose a new technique for hardware synthesis from higher-order functional languages with imperative features based on Reynolds Syntactic Control of Interference. The restriction on contraction in the type system is useful for managing the thorny issue of sharing of physical circuits. We use a semantic model inspired by game semantics and the geometry of interaction, and express it directly as a certain class of digital circuits that form a cartesian, monoidal-closed category. A soundness result is given, which is also a correctness result for the compilation technique.

The extraction of accurate finite-state models of higher-order or open programs is a difficult problem. We show how it can be addressed using newly developed game-semantic techniques and illustrate the solution with a model-checking tool based on such techniques. The approach has several important advantages over more traditional ones: precise account of inter-procedural behaviour, concise procedure summaries and surprising compactness of the extracted models.

We present a procedure for game-based model checking of an interesting fragment of Idealised Algol. The procedure requires only that the user state the safety property of interest. It than automatically generates abstractions of open program fragment (i.e. term-in-context) using iterative refinement. We have built a tool which implements the procedure. Its effectiveness is evaluated on several examples.

We consider a finitary procedural programming language (finite data-types, no recursion) extended with parallel composition and binary semaphores. Having first shown that may-equivalence of second-order open terms is undecidable we set out to find a framework in which decidability can be regained with minimum loss of expressivity. To that end we define an annotated type system that controls the number of concurrent threads created by terms and give a fully abstract game semantics for the notion of equivalence induced by typable terms and contexts. Finally, we show that the semantics of all typable terms, at any order and in the presence of iteration, admits a regular-language representation and thus the restricted observational equivalence is decidable.

This paper presents a semantic framework for data abstraction and refinement for verifying safety properties of open programs. The presentation is focused on an Algol-like programming language that incorporates data abstraction in its syntax. The fully abstract game semantics of the language is used for model-checking safety properties, and an interaction-sequence-based semantics is used for interpreting potentially spurious counterexamples and computing refined abstractions for the next iteration. An implementation based on the FDR model checker demonstrates practicality of the method.

We present a games-based denotational semantics for a quantitative analysis of programming languages. We define a Hyland-Ong-style games framework called slot games, which consists of HO games augmented with a new action called token. We develop a slot-game model for the language Idealized Concurrent Algol by instrumenting the strategies in its HO game model with token actions. We show that the slot-game model is a denotational semantics induced by a notion of observation formalized in the operational theory of improvement of Sands, and we give a full abstraction result. A quantitative analysis of programs has many potential applications, from compiler optimizations to resource-constrained execution and static performance profiling. We illustrate several such applications with putative examples that would be nevertheless difficult, if not impossible, to handle using known operational techniques.

We consider a finitary procedural programming language (finite data-types, no recursion) extended with parallel composition and binary semaphores. Having first shown that may-equivalence of second-order open terms is undecidable we set out to find a framework in which decidability can be regained with minimum loss of expressivity. To that end we define an annotated type system that controls the number of concurrent threads created by terms and give a fully abstract game semantics for the notion of equivalence induced by typable terms and contexts. Finally, we show that the semantics of all typable terms, at any order and in the presence of iteration, admits a regular-language representation and thus the restricted observational equivalence is decidable.

We introduce nominal games for modelling programming languages with dynamically generated local names, as examplified by Pitts and Stark's nu-calculus. Inspired by Pitts and Gabbay's recent work on nominal sets, we construct arenas and strategies in the world (or topos) of Fraenkel-Mostowski sets. This approach leads to a clean and precise treatment of fresh names and standard game constructions that are considered invariant under renaming. The main result is the construction of the first fully-abstract model of for the nu-calculus

We describe a software model checking tool founded on game semantics, highlight the underpinning theoretical results and discuss several case studies. The tool is based on an interpretation algorithm defined compositionally on syntax and thus can also handle open programs. Moreover, the models it produces are observationally fully abstract. These features are essential in the modeling and verification of software components such as modules and turn out to lead to very compact models of programs.

We are presenting a semantic analysis of Reynolds's specification logic of Idealized Algol using the parametric operational techniques developed by Pitts. We hope that this more elementary account will make the insights of Tennent and O'Hearn, originally formulated in a functor-category denotational semantics, more accessible to a wider audience. The operational model makes clearer the special nature of term equivalence in the logical setting, identifies some problems in the previous interpretation of negation and also proves the soundness of two new axioms of specification logic. Using the model we show that even a very restricted fragment of specification logic is undecidable.

We introduce a game model for a procedural programming language extended with primitives for parallel composition and synchronization on binary semaphores. The model uses an interleaved version of Hyland-Ong-style games, where most of the original combinatorial constraints on positions are replaced with a simple principle naturally related to static process creation. The model is fully abstract for may-equivalence.

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, regular-language semantics, which is a representation of the fully-abstract 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.

We explain how recent developments in game semantics can be applied to reasoning about equivalence of terms in a non-trivial fragment of Idealized Algol (IA) by expressing sets of complete plays as regular languages. Being derived directly from the fully abstract game semantics for IA, our model inherits its good theoretical properties; in fact, for first order IA taken as a stand-alone language the regular language model is fully abstract. The method is algorithmic and formal, which makes it suitable for automation. We show how reasoning is carried out using a meta-language of extended regular expressions, a language for which equivalence is decidable.

Two previous papers of the author show how finitary imperative procedural languages can be modeled using regular languages only, which are representation of fully abstract game models. This paper examines the possibility of using these models as a basis for model-checking Hoare-style partial correctness statements in such languages.

We give a fully abstract regular language model for a first-order CBV programming language, which is a representation of its fully abstract game model.

We explain how we can reason about equivalence of terms in a non-trivial fragment of IA by expressing sets of complete plays from the game semantic model as regular languages. The model is fully abstract, concrete and formal , which makes it uniquely suitable for automation. We show how reasoning can be carried out in a meta-language of regular expressions, for which equivalence is decidable.

A survey of the concept of state in programming languages.

A functor-category semantics for pointers.