Game Semantics for Java Programs

Although software verification has made great strides in the last few decades, it is well understood that
there is still a significant gap between the need and the supply of verification methods and tools.
In particular, methods which enjoy high accuracy and can scale up to the size of realistic applications
are extremely rare.

In this situation, methods stemming from the field of denotational semantics, which studies mathematical
models of programs using elements of set theory and logic, seem naturally advantageous. The denotational
approach uniquely combines two desirable features: abstraction and compositionality. Abstraction means
that the analysis focusses only on the observable aspects of program behaviour and is therefore bound
to lead to concise models. On the other hand, compositionality allows for large verification tasks to be broken
into constituent parts, which can then be solved separately.

The aim of this project is to use game semantics in order to devise models, prototype methods and tools
for Java programs. Game semantics is a denotational theory describing computation as a game: a dialogue
between the program and its environment which follows their exchange of data during program execution.
Games strike a balance between abstract mathematical models and operational techniques. They precisely
capture observable program behaviour but also provide models which have concrete representations and
are therefore amenable to algorihmic reasoning and automation. As a result, games constitute a natural
candidate for a refined semantics on which to base program verification.

Research in game semantics has recently made an important breakthrough towards the modelling of realistic
programming languages, with the introduction of a novel strand of the theory called Nominal Game Semantics.
Nominal games pinpoint dynamic program behaviours involving the generation of new resources, such as
reference names, objects, channels, etc. Moreover, research in automata over infinite alphabets has produced
machines with the potential of standing as algorithmic counterparts to nominal games. These developments
place us in a powerful position to attack Java, a mainstream language featuring such dynamic generative effects.

Our goal is to make an important step in devising disciplined, systematic and automated methods that bear
the potential to address difficulties not tackled by the state of the art and eventually lead to the development
of better software.

Software systems have become an integral part of the infrastructure of our society and control almost
every aspect of our lifestyles. Hence, verification and correctness are nowadays far from a marginal
software requirement concerning solely safety-critical systems. Rather, they are desiderata of software
development in general: they concern widespread applications written in mainstream languages.
The verification problem for such languages poses new challenges as high-level programming features
(references, objects, classes, etc) need to be handled accurately. Moreover, realistic applications can
expand to million lines of code, thus demanding highly scalable methods.

Our project aims at the definition and prototype implementation of a new methodology for modelling
and verifying Java programs. Because of its novel ingredients, notably, emphasis on compositionality
and focus on modelling only observable program behaviour, we hope to contribute foundations that
will influence verification standards. By adopting more refined semantic models, we give space to
methods which start from a higher level of accuracy and abstraction. By founding our approach on
compositional models, we anticipate substantial gains in scalability.

Because of the popularity of Java in industrial applications, the development of verification methods
and tools for Java programs is of major interest to the industry. We envisage that our project will lay
the foundations for a new wave of techniques making use of the benefits of the more refined models
that game semantics can provide.

In order to inform all interested parties about our approach, we have planned regular attendance at
the relevant conferences and workshops, research visits to groups pursuing related state-of-the-art
research based on alternative approaches, as well as the organisation of a workshop devoted to
modelling and verifying Java code. The event has been scheduled for the end of the first year of
the project. It will coincide with the expected completion of the modelling work package, when it is
already possible to convey the flavour of our approach. The workshop will also enable us to gather
feedback that can still be taken into account during the second implementation-oriented year
of the project. Further interaction links will be opened through subsequent visits to academic and
industrial labs to give presentations. To that end we are going to exploit existing academic
(e.g. Wessex Theory, East London Massive) and industrial (e.g. Microsoft, Monoidics) links at both
sites as well as personal contacts made at conferences.

As our project is of foundational nature, the main short-term beneficiaries will be other researchers
in industry and academia. In the longer run, we would like to see our modelling methods incorporated
into modelling engines of mainstream verification tools. Ultimately, we expect the work to impact
actual system developers and, consequently, users at large.