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.

Scope

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
   

Venue

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)
   

Submissions

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

https://www.easychair.org/login.cgi?conf=vstte10.

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

http://www.springer.de/comp/lncs/authors.html,

is strongly encouraged.

Workshops

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.

Competition

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

programs.

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