WING 2014 – 5th International Workshop on Invariant Generation
July 23, 2014 · Vienna, Austria
Important Dates
| Submission deadline | April 15, 2014 |
| Notification of acceptance | May 8, 2014 |
| Final version due | May 22, 2014 |
| Workshop | July 23, 2014 |
About WING
The ability to automatically extract and synthesize auxiliary properties of programs has had a profound effect on program analysis, testing, and verification over the last several decades. A key impediment for program verification is the overhead associated with providing, debugging, and verifying auxiliary invariant annotations. Releasing the software developer from this burden is crucial for ensuring the practical relevance of program verification. In the context of testing, suitable invariants have the potential of enabling high-coverage test-case generation. Thus, invariant generation is a key ingredient in a broad spectrum of tools that help to improve program reliability and understanding. As the design and implementation of reliable software remains an important issue, any progress in this area will have a significant impact.
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 Groebner bases, quantifier elimination, and algorithmic combinatorics, which can be used in conjunction with model checking, theorem proving, static analysis, and abstract interpretation. The aim of this workshop is to bring together researchers from these diverse fields.
Aims and Scope
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
- Deriving Assertions
- Inductive Proofs for Reasoning about Loops
- Applications to Assertion Generation using the following tools:
- Abstract Interpretation,
- Static Analysis,
- Model Checking,
- Theorem Proving,
- Theory Formation,
- Algebraic Techniques
- Tools for inductive assertion generation and verification
- Alternative techniques for reasoning about loops
Paper Submissions
We encourage submissions on work in progress, new ideas, tools under development, as well as work by PhD students, to be presented at WING 2014. Submissions should adhere to the EasyChair document class, and be between 6 and 15 pages.
Submissions need not be original. Extended versions of submissions may have been published previously, or submitted concurrently with or after WING 2014 to another workshop, conference or a journal.
Submit your paper here!
Program Committee
- Stephan Falke (Karlsruhe Institute of Technology (KIT))
- Carlo A. Furia (ETH Zurich)
- Arie Gurfinkel (Software Engineering Institute, Carnegie Mellon University)
- Dilian Gurov (Royal Institute of Technology (KTH))
- Reiner Hähnle (TU Darmstadt) - chair
- Andrew Ireland (Heriot-Watt University)
- Bart Jacobs (Katholieke Universiteit Leuven, Belgium)
- Einar Broch Johnsen (University of Oslo) - chair
- Laura Kovacs (Chalmers University of Technology)
- Enric Rodríguez Carbonell (Technical University of Catalonia)
- Philipp Ruemmer (Uppsala University, Department of Information Technology)