Verified Software:

Theories, Tools and Experiments

16th-19th August


Edinburgh, Scotland


The THEORY Workshop at VSTTE 2010


Program verification has seen a worldwide renaissance, with many practical tool projects and experimental verification efforts ongoing. The current state of the field builds on fundamental theoretical advances of the past. Similarly, future advances on software verification will depend on developments in theory. This can 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.

The Verified Software Initiative (VSI) is envisaged as a fifteen year "grand challenge" project to advance the state of software verification. Specific milestones and challenges of the VSI should often be concrete in nature, but advances beyond immediate progress will again depend on theoretical insights. The purpose of this workshop is to bring together theory and programming language researchers to discuss scientific challenges posed by software verification.

Call for papers

VS-THEORY 2010 invites submissions of technical papers of up to 10 pages (LNCS format) related to software verification in a broad sense. This includes research on proof methods for various programming paradigms (object-oriented, functional, imperative, concurrent, etc.), program/proof codesign, requirements modeling, specification languages, formal calculi, programming languages, language semantics, software design methods, software testing, automatic code generation, meta-programming and multi-stage computation, refinement methodologies, type systems, computer security, model checking and theorem proving. Evaluations, comparisons, and unification of rival methods are welcome. This list of topics is indicative, and is explicitly intended to be non-exhaustive.

In addition to technical papers we welcome challenge papers, up to 5 pages, that pose specific or general problems in theory that pertain to VSI. Such submissions should have the word "challenge" in their title.

Accepted papers will be made available online as an informal proceedings, but there will be no formal proceedings so publication elsewhere is not precluded.

Papers should be submitted via Easychair.

Important Dates

Submission deadline: 21 May 28 May

Notification of acceptance:  25 June

Final versions due: 23 July

Workshop: 18 August


The THEORY Workshop is part of VSTTE 2010 which will take place in Edinburgh.

Program committee

Amal Ahmed, Indiana University, US

Rajeev Alur, University of Pennsylvania, US

Anupam Datta, Carnegie Mellon University, US

Yannis Kassios, ETH Zurich, CH

Neel Krishnaswami, Microsoft Research, UK

Daniel Kroening, Oxford University, UK

Antoine Mine, CNRS, FR

Aleks Nanevski, IMDEA Software, SP

David Naumann, Stevens Institute of Technology, US (co-chair)

Tamara Rezk, INRIA, FR

Dave Schmidt, Kansas State University, US

Ashish Tiwari, SRI International, US

Viktor Vafeiadis, University of Cambridge, UK

Hongseok Yang, Queen Mary University of London, UK (co-chair)