https://www.dagstuhl.de/10252

June 20 – 25 , 2010, Dagstuhl Seminar 10252

Game Semantics and Program Verification

Organizers

Paul-Andre Mellies (University Paris-Diderot, FR)
Andrzej Murawski (University of Oxford, GB)
Andrea Schalk (University of Manchester, GB)
Igor Walukiewicz (University of Bordeaux, FR)

For support, please contact

Dagstuhl Service Team

Documents

List of Participants
Dagstuhl Seminar Schedule [pdf]

Summary

The seminar took place from 20th until 25th June 2010. Its primary aim was to bring together researchers working on modelling programs/proofs using games and the verification community. It was clear to us that both communities could, at this point in time, begin to profit from the methods and insights gained by the other community, and be able to help with some of the other side's unsolved problems. So far the two groups have had very little interaction with each other, although there are some researchers who are active in both areas. We organized the schedules on a day-to-day basis, in order to be as reactive as possible to the requests and questions coming from the discussions. We were also careful to leave a lot of time for interaction, while offering most participants the opportunity to give a talk. Twenty-two talks were delivered during the meeting.

The field of program verification aims to identify and implement techniques for automatic certification of program correctness or desirable program behaviour. A central task in any software verification project is the choice of a modelling approach and a decidable formalism in which the model will be represented for the purpose of verification.

Game semantics uses the metaphor of game playing to interpret computation, which it views as an exchange of moves between two players. This allows for a very concrete account of interaction consisting of sequences of moves, one that can be readily represented with common formalisms used in verification. As it turns out, this opens up the way to numerous applications. On the more abstract level, game semantics -- as a modelling technique -- offers a sophisticated abstraction mechanism, which enables one to describe what is observable in a program behaviour rather than what internal symbolic steps the programs make.

The atmosphere during the seminar was very good, clearly all the participants were open to new ideas from `the other side'. In particular the introductory talks attracted a number of questions asking for clarification on various issues. This showed us as the organizers that people were keen to understand the material that was presented to them, and that our selection of topics was suitable for our purposes. The periods we left unscheduled as well as the meals were then available for further discussion. In particular the young researchers present expressed their delight with the opportunity to talk to established participants in a relaxed atmosphere. Because this was a residential workshop, people did not have to worry about returning to their accommodation, or making arrangements for meals, which greatly facilitated smaller groups having additional discussions, of which we saw quite a few.

The Dagstuhl staff were extremely helpful throughout the meeting and, because most of the organizational tasks were carried out by them, the participants could concentrate on scientific matters. As the organizers we were very grateful for all the support! A number of people also commented positively on this aspect in their feedback forms.

It is perhaps too early to say how much of an impact our seminar will ultimately have. Because for many participants this was the first sustained encounter with the other community, it will take some time for ideas to be digested and adopted. The main achievement of the meeting is the creation of a platform on which new collaborations can be built in the years to come, leading to even more synergy between game semantics and verification.

Classification

  • Semantics / Formal Methods
  • Verification / Logic

Keywords

  • Static analysis
  • Automated verification
  • Semantics of programming languages

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.