https://www.dagstuhl.de/06281

July 9 – 13 , 2006, Dagstuhl Seminar 06281

The Challenge of Software Verification

Organizers

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)


The Dagstuhl Foundation gratefully acknowledges the donation from:

  •   Microsoft Research, Cambridge, UK

For support, please contact

Dagstuhl Service Team

Documents

List of Participants
Dagstuhl's Impact: Documents available

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.

Classification

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

Keywords

  • Mechanical Software Verification
  • Proof

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.

NSF young researcher support