Dagstuhl Seminar 10252
Game Semantics and Program Verification
( Jun 20 – Jun 25, 2010 )
- 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)
- Simone Schilke (for administrative matters)
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.
- Pierre Clairambault (CNRS - Paris, FR) [dblp]
- Ugo Dal Lago (University of Bologna, IT) [dblp]
- Ilias Garnier (Commissariat a l´Energie Atomique - Gif-sur-Yvette, FR)
- Dan R. Ghica (University of Birmingham, GB) [dblp]
- Alexis Goyet (CNRS - Paris, FR)
- Charles Grellois (ENS - Cachan, FR)
- Julian Gutierrez (University of Edinburgh, GB) [dblp]
- Peter Habermehl (University of Paris VII, FR) [dblp]
- Martin Hofmann (LMU München, DE) [dblp]
- Stefan Kiefer (University of Oxford, GB) [dblp]
- Naoki Kobayashi (Tohoku University - Sendai, JP) [dblp]
- James Laird (University of Bath, GB) [dblp]
- Olivier Laurent (ENS - Lyon, FR)
- Jérôme Leroux (University of Bordeaux, FR) [dblp]
- Paul Blain Levy (University of Birmingham, GB) [dblp]
- Etienne Lozes (ENS - Cachan, FR)
- Paul-Andre Mellies (University Paris-Diderot, FR) [dblp]
- Markus Müller-Olm (Universität Münster, DE) [dblp]
- Andrzej Murawski (University of Oxford, GB) [dblp]
- Damian Niwinski (University of Warsaw, PL) [dblp]
- Andrea Schalk (University of Manchester, GB)
- Helmut Seidl (TU München, DE) [dblp]
- Ian Stark (University of Edinburgh, GB) [dblp]
- Grégoire Sutre (University of Bordeaux, FR) [dblp]
- Nikos Tzevelekos (University of Oxford, GB) [dblp]
- Pawel Urzyczyn (University of Warsaw, PL) [dblp]
- Noam Zeilberger (University Paris-Diderot, FR)
- Lijun Zhang (Technical University of Denmark - Lyngby, DK) [dblp]
- semantics / formal methods
- verification / logic
- static analysis
- automated verification
- semantics of programming languages