Workshop on
Verified Software: Theories, Tools, and Experiments

This one-day FLoC 2006 workshop on Verified Software continues the discussion initiated at the IFIP Working Conference on Verified Software in Zurich, Switzerland.  Consisting of contributed papers and invited talks, the workshop will focus on the development of systematic methods for specifying, building, and verifying high-quality software. This includes topics like:

• Program logic
• Specification and verification techniques
• Design methodologies
• Automated verification tools
• Tool integration
• Achieving scale and automation in formal verification
• Experimental studies
• Benchmark applications and challenges
• Tool and benchmark repositories

The contributed papers, which should report on previously unpublished work, can reflect current and preliminary work in areas of software verification. New technical results, overviews of new developments in software verification projects, short papers accompanying tool demonstrations, as well as position papers on how to further advance the goal of verified software are all welcome. The papers can be up to 8 pages in length (in any reasonable format). Papers are submitted at http://www.easychair.org/VSTTE2006/.

The workshop registration and submission process is open to everyone.

Important dates

• Submission deadline:  1 June 2006
• Notification of acceptance:  9 June 2006
• Final version due:  7 July 2006
• Day of workshop:  22 August 2006

Proceedings of the workshop will be published as a Microsoft Research technical report.

Invited speakers

• Challenges and Lessons for Software Verification

  Dr. Jim Grundy, Research Scientist
  Strategic CAD Labs, Intel Corporation

  Abstract:
  Intel was an early and extensive adopter of formal verification technology for its hardware designs. In this talk I will attempt to relate a number of lessons from our experience to the endeavor of software verification. In particular I will present thoughts on

  • which application areas for software verification are likely to have the most commercial impact in the short term
  • commercially viable hardware verification techniques that are under represented in software verification research
  • differences between academic and commercial verification practice, and what this tells us about how to make software verification more economically compelling
  I will conclude with some thoughts on how the Intel experience of formal hardware verification relates to the VSTTE Grand Challenge Project proposed by Hoare and Misra.

  Speakers's bio:
  Jim is an active researcher in the application of interactive mechanical reasoning systems to verification problems in computer hardware and software, and in the development of mechanical reasoning systems for this purpose. He also maintains an interest in the presentation of proofs for human readers and in programming paradigms and languages.

  Jim joined the Logic Team in Intel's Strategic CAD Labs in 2000. He received a Bachelors degree with first class honors in Computer Science and a University Medal from the University of Queensland in 1989. He received a Doctoral degree from the University of Cambridge in 1994. Jim has worked as a post-doctoral researcher at Åbo Akademi University in Finland and as a research scientist at the Australian Defence Science & Technology Organisation. Prior to joining Intel, Jim was on the faculty at the Australian National University. Jim is a member of the ACM and a senior member of the IEEE.

Program committee

• Marieke Huisman, INRIA Sophia Antipolis, France
• K. Rustan M. Leino (co-chair), Microsoft Research, USA
• Claude Marché, Université Paris-Sud, France
• Wolfgang J. Paul, Saarland University, Germany
• Wolfram Schulte (co-chair), Microsoft Research, USA
• Cesare Tinelli, University of Iowa, USA
• Arnaud Venet, Kestrel Technologies, USA

Sponsoring Conference

CAV 2006