09. – 13. Juli 2006, Dagstuhl-Seminar 06281

The Challenge of Software Verification


Manfred Broy (TU München, DE)
Patrick Cousot (ENS – Paris, FR)
Jayadev Misra (University of Texas – Austin, US)
Peter O'Hearn (Queen Mary University of London, GB)

Die Dagstuhl-Stiftung erhielt eine Spende von:

  •   Microsoft Research, Cambridge, UK

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl's Impact: Dokumente verfügbar

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.


  • Programming Languages / Compiler
  • Sw-engineering Semantics / Formal Methods
  • Verification / Logic


  • Mechanical Software Verification
  • Proof


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.