Welcome to WING 2009!

Satellite Workshop of ETAPS 2009

Program verification has a long research tradition, but so far its impact on development of safety critical software has been relatively limited. A key impediment has been the overhead associated with providing and debugging auxiliary invariant annotations. As the design and implementation of reliable software remains an important issue, any progress in this area will be of utmost importance for future developments in IT.

The logically deep parts of the code are characterized by (nested) loops or recursions. For these parts, formal program verification is an appropriate tool. One of its biggest challenges is automated discovery of inductive assertions, leading to verification of safety and security properties of programs.

The increasing power of automated theorem proving and computer algebra has opened new perspectives for computer aided program verification; in particular for the automatic generation of inductive assertions in order to reason about loops and recursion. Especially promising breakthroughs are invariant generation techniques by Gröbner bases, quantifier elimination, and algorithmic combinatorics, which can be used in conjunction with model checking, theorem proving, static analysis and abstract interpretation.

Scope

This workshop aims to bring together researchers from several fields of abstract interpretation, computational logic and computer algebra to support reasoning about loops, in particular, by using algorithmic combinatorics, narrowing/widening techniques, static analysis, polynomial algebra, quantifier elimination and model checking.

We encourage submissions presenting work in progress, tools under development, as well as research of PhD students, such that the workshop can become a forum for active dialog between the groups involved in this new research area.

Relevant topics include (but are not limited to) the following:

• Program analysis and verification
• Inductive Assertion Generation
• Inductive Proofs for Reasoning about Loops
• Applications to Assertion Generation using the following tools:
• Abstract Interpretation
• Static Analysis
• Model Checking
• Theorem Proving
• Algebraic Techniques
• Tools for inductive assertion generation and verification
• Alternative techniques for reasoning about loops

Publication

All submissions will be peer-reviewed by the programme committee. Accepted contributions will be published in archived electronic notes, as an EasyChair collection volume.

A special issue of the Journal of Symbolic Computation with full versions of selected papers will be published after the workshop.

Keynote Speakers

Leonardo de Moura (Microsoft Research, USA)

Andrey Rybalchenko (MPI-SWS, Germany)

Program Chairs

Andrew Ireland (Heriot-Watt University, UK)

Laura Kovács (EPFL, Switzerland)

Program Committee

Nikolaj Bjørner (Microsoft Research, USA)

Martin Giese (University of Oslo, Norway)

Reiner Hähnle (Chalmers University of Technology, Sweden)

Paul Jackson (University of Edinburgh, UK)

Jens Knoop (Technical University of Vienna, Austria)

Francesco Logozzo (Microsoft Research, USA)

Wolfgang Schreiner (RISC-Linz, Austria)

Helmut Veith (Technical University of Darmstadt, Germany)

Andrei Voronkov (Manchester University, UK)

Thomas Wies (EPFL, Switzerland)

Important Dates

Page maintained by Laura Kovács.