Verified Software: Theories, Tools, Experiments

Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to the latest Netscape.
More information

Conference Report
print page

The IFIP Working Conference on Verified Software: Theories, Tools, Experiments

Tony Hoare, Jayadev Misra, and N. Shankar
October 20, 2005

PDF Version

The IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE; was held at Zurich, Switzerland, during Oct 10-13, 2005. The goal of the conference was to establish a concrete plan of action for taking on Professor Tony Hoare?s proposal of verified software as a Grand Challenge for research in computing. The conference was hosted and organized by Professor Bertrand Meyer, Chair of Software Engineering, ETH Zurich, as part of the 150th anniversary celebration of this august institution, and cosponsored by IFIP Working Group 2.3. Financial support for the meeting came from ETH Zurich, the National Coordination Office for Networking and Information Technology Research through the National Science Foundation of USA, Microsoft Research (Cambridge), and the Engineering and Physical Research Council of UK.

The meeting included

The VSTTE Working Conference yielded a good consensus on the shape of the Grand Challenge and the nature of the theories, tools, and experiments needed to achieve success in the envisioned fifteen-year time-frame. A number of relevant and interesting challenges have been identified, on varying scales and different degrees of difficulty. The more straightforward ones could be tackled immediately by existing tools, and might serve as useful pilot projects before the main work of the Challenge starts. Examples include a lightweight file system, embedded system controllers, and medical devices. The Grand Challenge activity will be centered around a digital repository containing a suite of tools, reference specifications and semantics, and challenge codes with specifications and annotations. Another focus will be the design of a formal tool bus to mediate the coarse-grained interaction between a variety of syntactic and semantic tools to support verification activity. The conference ended by setting up a number of specialist panels that will draft ideas for concrete projects and research directions which will lead to ultimate success. Panel topics include

  1. Integral Verification Systems
  2. Digital Repository and Challenge Codes Theory
  3. Correctness by Construction
  4. System Certification
  5. Tool Integration and Interoperability

An Advisory Board will supervise the activities of the topical panels. Attendants at the conference are encouraged to organise sessions and workshops on verified software on the next occasion that they attend a conference in one of the recognised national or international series. Such workshops encourage members of the individual communities to direct and extend and apply their distinctive research skills towards the goals of the project.

With the success of the VSTTE Working Conference, we are optimistic that the Verified Software grand challenge will stimulate advances in software specification, software design methods, programming language design and semantics, and program analysis and verification technology that can have a dramatic impact on the engineering of reliable software with reduced lifetime costs.