Scope and Objectives

The goal of the conference is to discuss steps on the long road towards the creation of verified software. It is a forum to discuss prospects for collaborative development of mechanised tools for the formal development and verification of computer programs. It addresses the experimental evaluation of the tools by competitive trials on an agreed collection of practically useful programs. In the end, the conference should work towards the achievement of the long-standing challenge of the Verifying Compiler.

The Grand Challenge

The VSTTE conference took off from Tony Hoare's "grand challenge" concept. Tony and Jay Misra have written a paper describing the issues at stake. Conference participants and others interested in the topic are encouraged to use the associated Wiki page to share their comments.

Topics and Questions

Program Analysis: control and data flow, alias analysis, abstract syntax trees, type inference, verification condition generation, invariant assertion inference, test case generation and selection, program development environments, programmer productivity tools

Can these be integrated as an effective research toll for program verification?

Theorem Proving: constraint solving, counter-examples, resolution, model checking, algebraic reduction, inductive hypothesis generation, theory libraries, code generation, correctness-preserving optimisation

Can these be developed for application to actual program verification?

Challenge codes specifications: smartcards, embedded systems, industrial control, web services, open sources, commercial off-the-shelf software, common base libraries and APIs, operating system kernels, mixed language programs, generated programs; together with their specifications, design histories, assertions, verification conditions, conjectures, theorems, redusable theories, test cases and other documentation

What sample is suitable for evaluation/development of verification tools?

Semantics of correctness: object orientation, inheritance, exceptions, concurrency, process algebra, mixed languages, interfaces to spread sheets and data bases, design patterns, aspects, distribution, architecture

Can programming theory yet fully explain why real big programs work?

Common internal formats: requirements, specifications, modelling languages, programs, internal compiler interfaces, abstract syntax trees, intermediate languages

Will it be possible to develop a coherent tool-set by international collaboration?

Non-functional properties: requirements, security, trust, dependability, fault tolerance, fault avoidance, HCI, reliability metrics, software evolution

Can verification technology and tools be applied more widely to these properties?

State of the art: history, current industrial applications and achievements, promising developments in any of the enabling technologies

Do current achievements and trends predict success for a verifying compiler?