Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 06281

The Challenge of Software Verification

( Jul 09 – Jul 13, 2006 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:


The Dagstuhl Foundation gratefully acknowledges the donation from

Contents and Aims of Seminar

Correctness of programs is a fundamental conceptual issue in computer science. But, ever since the basic works on correctness in the 1960s by Floyd, Hoare and Naur there has been a looming question: could mechanical verification be made viable, cost-effective for a wide range of software?

Throughout the world there is renewed excitement on the problem of mechanical verification of software. This can be seen in the development of software model checkers and expressive static analyses, in experimental programming languages that go beyond traditional typechecking by including assertions as part of their designs, as well as in the more traditional realms of machine-assisted proof and program construction by refinement. The purpose of this workshop is to bring together leading researchers to discuss the scientific challenge posed by software verification.

This is part of an effort at formulating a possible 15-year Grand Challenge in computer science on the problem of software verification. Several preliminary workshops on the topic have been held in the UK and US, and an international meeting on the topic was held as an IFIP working conference “Verifies Software: Tools, Theories and Experiments” in Zurich in October of 2005. A number of small commitees were charged with discussing and reporting on questions from the IFIP conference (e.g., on future work for theories, proof tools, tool integration), and presentations on these will be given at the Dagstuhl workshop.

This Dagstuhl meeting will give European researchers a chance to meet and develop their position regarding the challenge of software verification (complementing an NSF-sponsored workshop oriented to US researchers held in February 2005). That is one part of the workshop’s motivation, but the overall project, and participation in this meeting, is international in nature.

A major focus of the workshop will be on understanding the state of the art in mechanical verification of industrial-scale systems, and we will invite people who have actually written and delivered code that has been proved manually or with partial machine assistance. Candidate projects include mission, safety, and securitycritical applications, such as the IBM CICS transaction-processing and the Mondex smart card system, as well as common system components such as file systems or even operating system kernels. Participants will be invited to contribute to this and report their findings at the workshop. After the workshop finishes we plan on producing a document outlining the current state, with an emphasis on specific practical projects, and with a view to how it might inform any future international grand challenge.

In addition to “experience talks” describing actual use of verification technology, we will also solicit presentations on challenge codes for future verification efforts. An example might be to establish the structural integrity of selected open-source infrastructure software, perhaps leading to the crash-proofing of a web server, or an operating system, or even the entire internet. Other than this, and the IFIP reports, the workshop structure will be informal, not overspecified in advance.

  • Jean-Raymond Abrial (ETH Zürich, CH) [dblp]
  • Anindya Banerjee (Kansas State University, US) [dblp]
  • Gilles Barthe (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
  • Bernhard Beckert (Universität Koblenz-Landau, DE) [dblp]
  • Joshua Berdine (Microsoft Research UK - Cambridge, GB) [dblp]
  • Yves Bertot (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
  • Egon Börger (University of Pisa, IT) [dblp]
  • Richard Bornat (Middlesex University, GB) [dblp]
  • Manfred Broy (TU München, DE) [dblp]
  • Michael Butler (University of Southampton, GB) [dblp]
  • Cristiano Calcagno (Imperial College London, GB)
  • Rod Chapman (Praxis High Integrity Systems Ltd. - Bath, GB)
  • Byron Cook (Microsoft Research UK - Cambridge, GB) [dblp]
  • Patrick Cousot (ENS - Paris, FR) [dblp]
  • Reiner Hähnle (Chalmers UT - Göteborg, SE) [dblp]
  • Stefan Hallerstede (ETH Zürich, CH) [dblp]
  • Moritz Hammer (LMU München, DE)
  • Charles Anthony Richard Hoare (Microsoft Research UK - Cambridge, GB) [dblp]
  • Marieke Huisman (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
  • Dieter Hutter (DFKI - Saarbrücken, DE)
  • Bart Jacobs (Radboud University Nijmegen, NL) [dblp]
  • Cliff B. Jones (University of Newcastle, GB) [dblp]
  • Joseph Roland Kiniry (University College Dublin, IE) [dblp]
  • Daniel Kroening (ETH Zürich, CH) [dblp]
  • Gary T. Leavens (Iowa State University, US) [dblp]
  • K. Rustan M. Leino (Microsoft Research - Redmond, US) [dblp]
  • Etienne Lozes (ENS - Cachan, FR)
  • Tiziana Margaria (Universität Potsdam, DE) [dblp]
  • Bertrand Meyer (ETH Zürich, CH) [dblp]
  • Jayadev Misra (University of Texas - Austin, US)
  • C. Carroll Morgan (UNSW - Sydney, AU)
  • David A. Naumann (Stevens Institute of Technology, US) [dblp]
  • Tobias Nipkow (TU München, DE) [dblp]
  • Peter O'Hearn (Queen Mary University of London, GB) [dblp]
  • Wolfgang J. Paul (Universität des Saarlandes, DE) [dblp]
  • Lawrence Paulson (University of Cambridge, GB) [dblp]
  • Andreas Podelski (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Erik Poll (Radboud University Nijmegen, NL) [dblp]
  • Wolfgang Reif (Universität Augsburg, DE) [dblp]
  • Tamara Rezk (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
  • Peter H. Schmitt (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Kaisa Sere (Abo Akademi University - Turku, FI)
  • Natarajan Shankar (SRI - Menlo Park, US) [dblp]
  • Bernhard Steffen (TU Dortmund, DE) [dblp]
  • Andrzej Tarlecki (University of Warsaw, PL)
  • Pawel Urzyczyn (University of Warsaw, PL) [dblp]
  • Tarmo Uustalu (Technical University - Tallinn, EE) [dblp]
  • Helmut Veith (TU München, DE) [dblp]
  • Reinhard Wilhelm (Universität des Saarlandes, DE) [dblp]
  • James C. P. Woodcock (University of York, GB) [dblp]
  • Kwangkeun Yi (Seoul National University, KR) [dblp]

  • programming languages / compiler
  • sw-engineering semantics / formal methods
  • verification / logic

  • Mechanical Software Verification
  • Proof