Verified Software:

Theories, Tools and Experiments

16th-19th August


Edinburgh, Scotland


Call for Papers [text version]

The Third International Conference on Verified Software: Theories, Tools, and Experiments follows a successful inaugural working conference at Zurich (2005) and a successful conference in Toronto (2008). This conference is part of the Verified Software Initiative (VSI), a fifteen-year, cooperative, international project directed at the scientific challenges of large-scale software verification. VSI also includes UKCRC's Grand Challenge 6, i.e. Dependable Systems Evolution. VSTTE is open to anyone who is interested in participating actively in the VSI effort.


The goal of this conference is to advance the state of the art in the science and technology of software verification through the interaction of theory development, tool evolution, and experimental validation.  Authors are encouraged to submit work in progress, particularly if the work involves collaboration, theory unification, and tool integration.  Topics of interest include

  1.  requirements modeling

  2.  specification languages

  3.  specification/verification case-studies

  4.  formal calculi

  5.  programming languages

  6.  language semantics

  7.  software design methods

  8.  software testing

  9.  automatic code generation

  10.  refinement methodologies

  11.  type systems

  12.  computer security

  13.  verification tools (static analysis, dynamic analysis, model checking, theorem proving, satisfiability)

  14.  tool integration

  15.  benchmarks

  16.  challenge problems

  17.  integrated verification environments

We also encourage researchers to submit challenges in theory, formalization, systems verification, code verification, and applications. Contributions relating to existing challenges will also be welcomed, i.e.

  1. POPLMark

  2. Tokeneer

  3. POSIX file system

  4. medical devices


VSTTE 2010 is being hosted by Heriot-Watt University in Edinburgh. The conference dates coincide with the 2010 Edinburgh International Festival and the Edinburgh Festival Fringe -- collectively the largest annual  arts festival on the planet! The technical programme will take place in the Edinburgh Conference Centre (Riccarton campus), where accommodation will be available at very competitive rates for festival time. Social events will be arranged within the city centre, making VSTTE an unique cultural and scholarly event for 2010!

Invited Speakers

  1. Tom Ball (Microsoft Research, Redmond)

  2. Gerwin Klein (National ICT Australia)

  3. Matthew Parkinson (University of Cambridge)


Submitted research papers and system descriptions must be original and not submitted for publication elsewhere.  Research paper submissions are limited to 15 proceedings pages in LNCS format and must include a cogent and self-contained description of the ideas, methods and results, together with a comparison to existing work. System descriptions are also limited to 15 proceedings pages in LNCS format. Submissions of theoretical, practical, and experimental contributions are equally encouraged, including those that focus on specific problems or problem domains. Papers can be submitted at


Submissions that arrive late, are not in the proper format, or are too long will not be considered.  The proceedings of VSTTE 2010 will be published by Springer-Verlag in the LNCS series.  Authors of accepted papers will be requested to sign a form transferring copyright of their contribution to Springer-Verlag.  The use of LaTeX and the Springer llncs class files, obtainable from


is strongly encouraged.


In addition to the main conference, VSTTE will host two workshops on August 19th:

  1. VS-Theory focuses on theoretical foundations of software verification. Topics range from the difficult and essential study of soundness of delicate proof methods, to the discovery of new specification techniques and proof methods, to dramatic simplification or unification of existing methods, to as yet unknown breakthroughs.

  2. VS-Tools & Experiments focuses on the development of verification tools and their experimental evaluation. Possible topics include interfaces between tools, tool integration platforms, and case studies.

The workshops will provide a forum to present new, possibly unfinished work and will also give the opportunity to propose research challenges, which will help form a research agenda for the Verified Software Initiative.

Papers must be written in English using Springer LNCS style. The page limit is 10 pages for technical papers and 5 pages for proposals of verification challenges. The proceedings will be published as a technical report.

Important Dates

March 29, 2010: Conference paper submission deadline

May 10, 2010: Decisions on papers

May 28, 2010: Workshop paper submission

June 1, 2010: Final conference paper versions due

June 25, 2010: Notification on workshop papers

July 23, 2010: Final workshop paper version

August 16-18, 2010: Main conference

August 18-19, 2010: Workshops

Research Student Support

A limited number of grants, cover registration and travel, will be available to support PhD students wishing to attend VSTTE 2010. More details will follow shortly.

Summer school

There will be a two-day summer-school preceding the main conference on the 14 and 15 August. The summer school will give a broad overview of software verification techniques,  addressing both bottom-up and top-down approaches with a strong focus on the formal representation and reasoning themes. The school consists of eight introductory lectures, each concentrating on an unique aspect of one or both of the overall themes. The topics of the lectures include inductive theorem proving; SAT and SMT solving; proof planning and rippling; rely/guarantee conditions; separation logic; operating system verification; BiGraphs and formal analysis of security.

The following will present at the summer school:

  1. Robert Atkey (University of Strathclyde) & Ewen Maclean (Heriot-Watt University)

  2. Alan Bundy & Lucas Dixon (University of Edinburgh)

  3. Cliff Jones (University of Newcastle)

  4. Gerwin Klein (National ICT Australia)

  5. Robin Milner (University of Cambridge/Edinburgh)

  6. J Strother Moore (University of Texas at Austin)

  7. Natarajan Shankar (SRI)

  8. Graham Steel (INRIA)

The school is intended for PhD students and researchers working within one or both of these themes, however familiarity with any of the techniques is not a prerequisite. All lectures are meant to be introductory.  For more information follow this link.


A verification competition will be held at VSTTE 2010. The challenge is to develop a machine-verified piece of software with respect to a given specification. The competition will be conducted over a 2.5 hour period on some evening of the conference. The problem will be presented with a logical specification and test cases over .5 hours including time for discussion with 2 hours to construct a solution. Each competing team can feature up to three members. You can use any tool or combination of tools as well as libraries, but you cannot modify these tools.  You can reinterpret the specification to suit your tools and methods, but you will be judged on the fidelity of your interpretation. The goal is to produce an executable program and a replayable proof that the program meets the specification.  It will be possible to code the solution using integers and arrays. The solutions will be judged for soundness (absence of bugs) and completeness (presence of proofs). The three best solutions will be selected and the respective teams will be invited to make presentations at the tools/experiments workshop. You must register a copy of the  verification system with the judges prior to the competition with instructions for replaying proofs and running the


Conference Chair

Andrew Ireland (Heriot-Watt University)

Program Chairs

  1. Peter O'Hearn (Queen Mary, University of London)

  2. Gary T. Leavens (University of Central Florida)

  3. Sriram Rajamani (Microsoft Research)

Workshop General Chair

Peter Mueller (ETH Zurich)

Theory Workshop Chairs

David Naumann (Stevens Institute of Technology)

Hongseok Yang   (Queen Mary, University of London)

Tools & Experiments Workshop Chairs

Rajeev Joshi  (NASA JPL)

Tiziana Margaria (Universität Potsdam)

Publicity Chair

Gudmund Grov (University of Edinburgh)

Local Arrangements Chair

Ewen Maclean (Heriot-Watt University)

Program Committee

  1. Ahmed Bouajjani

  2. Leo Freitas

  3. Philippa Gardner

  4. John Hatcliff

  5. Ranjit Jhala

  6. Joseph Kiniry

  7. Rustan Leino

  8. Xavier Leroy

  9. David Naumann

  10. Matthew Parkinson

  11. Wolfgang Paul

  12. Shaz Qadeer

  13. Andrey Rybalchenko

  14. Augusto Sampaio

  15. Zhong Shao

  16. Aaron Stump

  17. Serdar Tasiran

  18. Willem Visser

  19. Chin Wei-Ngan

  20. Stephanie Weirich

  21. Greta Yorsh

Steering Committee

  1. Tony Hoare

  2. Jay Misra

  3. Natarajan Shankar

  4. Jim Woodcock