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.
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.
Submission deadline: 28 May
Notification of acceptance: 25 June
Final versions due: 23 July
Workshop: 19 August
The THEORY Workshop is part of VSTTE 2010 which will take place in Edinburgh.