Program Reasoning with Nominal Game Semantics

Lead Research Organisation: Queen Mary, University of London
Department Name: Sch of Electronic Eng & Computer Science

Abstract

While in recent years great strides have been made in software verification, most of these successes have targeted programming languages of a strong imperative flavour. However, there is an emerging class of languages using higher-order features to cater for well-structured and disciplined programming outputs, for which verification methods are very scarce. In such higher-order languages, capturing formally the behaviour of programs is highly non-trivial and, therefore, even simple program analysis tasks prove to be surprisingly daunting.

This project will combine the latest techniques from game semantics with successful verification approaches from the imperative setting in order to achieve a novel reasoning methodology for higher-order languages. Game semantics is a theory of computation that has emerged as a robust paradigm for assigning formal mathematical semantics to higher-order programs. Game models offer a particularly suitable foundation for program analysis as they combine two features of focal importance: abstraction and compositionality. The former is achieved by focussing only on observable program behaviours, which significantly reduces the examined state-space of programs. The latter amounts to modelling compound program phrases by canonically combining the models of their respective sub-phrases, which in turn allows for the independent analysis of program components and enables local reasoning techniques.

The major obstacle in applying game semantics to real program analysis has been the modelling of dynamic generative effects, involving the generation of fresh references, objects, channels, etc. This issue has been addressed by a recent breakthrough that introduced atomic objects, called "names", in games for representing datatypes of dynamically generated resources. Names led to the introduction of a new strand of the theory called Nominal Game Semantics. Nominal games have extended the reach of game models to realistic higher-order languages and have brought the field to the point where one can start developing formal reasoning methods for such languages.

Our research will take the theory of game semantics to the next level and apply it to program reasoning. Our aim is to derive practical program logics for higher-order programs, equipped with high-level rules enabling abstraction and local reasoning, and complement them with a prototype implementation. The overall vision behind this proposal is to exploit the strong handle on higher-order computation provided by the nominal approach to game semantics in order to significantly extend the reach of modern approaches to verification and aid the production of better software.

Planned Impact

Software systems have become an integral part of the infrastructure of our society and control almost every aspect of our lives. Hence, verification and correctness are nowadays far from marginal software requirements concerning solely safety-critical systems. Rather, they are desiderata of software development in general: they concern widespread applications written in a variety of programming languages. The verification problem for such languages poses new challenges as high-level programming features (references, higher-order functions, etc) require accurate handling. Moreover, realistic applications can expand to millions of lines of code, thus demanding decidedly scalable methods.

Our project will achieve the introduction and prototype implementation of a new methodology for reasoning about higher-order programs. Because of its novel ingredients, namely the combination of precise abstractions, compositionality and focus on local reasoning, we hope to contribute techniques 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 and reasoning in local environments, we anticipate substantial gains in scalability.

Higher-order programming languages have seen a surge of interest in recent years, with specific applications coming from security-sensitive domains like the finance sector. Hence, the development of verification methods and tools for such languages is of major interest to the industry. Until now, such methods and tools have been very scarce, as the analysis of higher-order programs is a daunting task. Our proposal aims at addressing this shortcoming using the unique advantages of program models obtained from game semantics, and nominal game semantics in particular.

In order to inform all interested parties about our approach, we have planned regular attendance of relevant conferences and workshops, research visits to groups pursuing related state-of-the-art research, and the organisation of a workshop devoted to program logics for higher-order program verification. The latter has been scheduled for the end of the first year of the project. It will coincide with the expected completion of the main tasks from the program logic work packages, when it will be possible to convey the core of our approach. Further connections will be made through visits to academic and industrial labs to give presentations. To that end we are going to exploit existing academic (e.g. Wessex Theory, Joint Theory Seminar) and industrial (e.g. Facebook, Microsoft) links at Queen Mary, as well as personal contacts made at conferences and the workshop.

As our project is of a foundational nature, the main short-term beneficiaries will be other researchers in academia and industry. In the longer term, we would like to see our approach incorporated into mainstream verification tools. Ultimately, we expect the work to impact actual system developers and, consequently, users at large.
 
Description This research further developed the application of game semantics as a foundational theory for reasoning about software.

It examined the behaviour of modern higher-order programming languages and in particular contributed new techniques for producing highly accurate models of programming languages with polymorphism and higher-order references.

Moreover, by incorporating ideas from game semantics and operational methods, it designed a novel method for proving equivalence of programs with higher-order references.

The project looked into the combination of game semantics with program logics and proved that separation logic techniques can be used to reason about intensional properties of higher-order programs, with games forming the underlying semantic backbone.
Exploitation Route This research revealed subtleties in the behaviour of polymorphic programs in the presence of references, which make their understanding and modelling particularly elaborate. Our modelling technique can be therefore used by others for modelling and reasoning about such programs.

The new technique introduced to reason about equivalence of programs opens the way to designing automatic methods for proving such equivalences, and to extensions to the polymorphic model we developed.

The application of separation logic on game-traces provides an example for the use of game semantics as a general-basis semantic theory for higher-order programs and, more concretely, a program reasoning method that can be put to use by the separation logic community.
Sectors Digital/Communication/Information Technologies (including Software)

 
Description EPSRC grant
Amount £326,972 (GBP)
Funding ID EP/P004172/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 01/2017 
End 12/2019
 
Title Nominal games for polymorphism and state 
Description We developed an operational game model for a polymorphic programming language with state, where names are used as abstract types and polymorphic values, and also as heap locations. 
Type Of Material Improvements to research infrastructure 
Year Produced 2016 
Provided To Others? Yes  
Impact Method was further extended to study System F parametricity. 
 
Description Aarhus 
Organisation Aarhus University
Department Department of Computer Science
Country Denmark 
Sector Academic/University 
PI Contribution Expertise and production of collaborative research
Collaborator Contribution Expertise and production of collaborative research
Impact Conference submission
Start Year 2015
 
Description Lyon 
Organisation University of Lyon
Country France 
Sector Academic/University 
PI Contribution Emanating from the project, the collaboration with Dr Jaber is still ongoing and we are currently collaborating on an adjacent research direction.
Collaborator Contribution Emanating from the project, the collaboration with Dr Jaber is still ongoing and we are currently collaborating on an adjacent research direction.
Impact Emanating from the project, the collaboration with Dr Jaber is still ongoing and we are currently collaborating on an adjacent research direction.
Start Year 2017