Workshop on Invariant Generation - WING 2010

This third International Workshop on Invariant Generation brings together researchers from abstract interpretation, computational logics, computer algebra and model checking to exchange their newest research on invariant generation techniques and applications.

Invariants are forever

The ability to extract and synthesize auxiliary properties of programs has had a profound effect on program analysis, testing and verification over the last several decades. The field of invariant generation draws on a multitude of techniques ranging from computer algebra, theorem proving, constraint solving, abstract interpretation techniques and model-checking. Likewise, are the application areas diversified from bootstrapping static program analysis tools, to test-case generation and into aiding the quest for verified software. So invariants are a key ingredient in program analysis and understanding. Yet, invariant generation poses as many challenges as promises: A key impediment for program verification is the overhead associated with providing, debugging, and verifying 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 verified software. In the context of static analysis and test-case generation, suitable invariants have the potential of enabling sophisticated automatic program analysis and high-coverage test-case generation.

Several modern techniques for program termination and expected program execution time also rely heavily on suitable invariants (as relations) for the termination analysis.

Automated discovery of inductive assertions is therefore one of the ultimate challenges for 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 Groebner 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

 

Program

--------------------
9:00-10:00: Session 1 - Invited Talk
Helmut Seidl: Abstract Interpretation Meets Mathematical Optimization

--------------------

10:00-10:30: Coffee break

--------------------
10:30-12:30: Session 2 - Regular Papers and Tool Demos
10:30-11:00: Stephane Gaubert, Ricardo Katz and Sergei Sergeev. 
        Tropical linear programming and parametric mean payoff games
11:00-11:22: Michael Franssen. 
        Cocktail II
11:22-11:44: Igor Konnov. 
        CheAPS: a Checker of Asynchronous Parameterized Systems
11:44-12:06: Ewen Maclean, Andrew Ireland and Gudmund Grov. 
        Synthesising Functional Invariants in Separation Logic
12:06-12:28: Florian Zuleger and Moritz Sinn. 
        LOOPUS - A Tool for Computing Loop Bounds for C Programs
--------------------

12:30-14:00: Lunch break

--------------------
14:00-15:00: Session 3 - Invited Talk
Sumit Gulwani: Methods for Loop Invariant Generation

--------------------

15:00-15:30: Coffee break
--------------------

15:30-17:30: Session 4: Regular Papers and Tool Demos
15:30-16:00: Matthias Kuntz, Stefan Leue and Christoph Scheben. 
        Extending Non-Termination Proof Techniques to Communicating Asynchronous Concurrent Programs
16:00-16:22: Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich and Christoph M. Wintersteiger. 
        Loopfrog — loop summarization for static analysis
16:22-16:44: Vlad Volkov, Alexander Letichevsky, Alexander Kolchin, Oleksandr Letychevskyy jr., Stepan Potiyenko and Thomas Weigert. 
        Formal Requirements Capturing using VRS system
16:44-17:06: Alexei Lisitsa. 
        Finite countermodels as invariants. A case study in verification of parameterized mutual exclusion protocol
17:06-17:28: Radu Iosif, Marius Bozga, Filip Konecny and Tomas Vojnar. 
        Tool Demonstration of the FLATA Counter Automata Toolset

Keynote Speakers:

Organizers:

Program Committee:

Important Dates

  March 19, 2010: Submission deadline
  April 23, 2010: Notification of acceptance  
  May 7, 2010: Camera-ready copy deadline
  July 21, 2010: WING 2010 in Edinburgh, UK

Submission

Submission will be via EasyChair.

Please submit research reports up to 15 pages in PDF,
conforming to the format produced by LaTeX using the
easychair.cls class file of EasyChair.
The class style may be downloaded at:

http://www.easychair.org/easychair.zip

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.