20. – 25. Juni 2010, Dagstuhl-Seminar 10252

Game Semantics and Program Verification


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)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS
Programm des Dagstuhl-Seminars [pdf]


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.


  • Semantics / Formal Methods
  • Verification / Logic


  • Static analysis
  • Automated verification
  • Semantics of programming languages


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.