[Please post - apologies for multiple copies.]

----------------------------------------------------
WING 2012 - 4th International Workshop on INvariant Generation
         http://cs.nyu.edu/acsys/wing2012/
                June 30, 2012
   Manchester, UK (a satellite Workshop of IJCAR 2012)
----------------------------------------------------
        --- First Call for Papers ---

General
-------

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.


Scope
-----

We encourage submissions presenting work in progress, tools under
development, as well as work by PhD students, such that the
workshop can become a forum for active dialogue 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,
- Theory Formation,
- Algebraic Techniques
* Tools for inductive assertion generation and verification
* Alternative techniques for reasoning about loops


Committee
-----------------

Program Chairs:

* Gudmund Grov (University of Edinburgh, UK)
* Thomas Wies (New York University, USA)

Program Committee:

* Clark Barrett (New York University, USA) 
* Nikolaj Bjorner (Microsoft Research, USA)
* Gudmund Grov (University of Edinburgh, UK)
* Ashutosh Gupta (IST Austria)
* Bart Jacobs (Katholieke Universiteit Leuven, Belgium) 
* Moa Johansson (Chalmers University of Technology, Sweden)
* Laura Kovacs (Vienna University of Technology, Austria)
* David Monniaux (VERIMAG, France)
* Enric Rodriguez Carbonell (Technical University of Catalonia, Spain) 
* Helmut Veith (Vienna University of Technology, Austria)
* Thomas Wies (New York University, USA)


Important Dates
---------------

Submission deadline: April 06, 2012
Notification of acceptance: May 04, 2012
Final version due: June 08, 2012
Workshop: June 30, 2012


Submission
----------

WING 2012 encourages submissions in the following two categories:

* Original papers: contain original research (simultaneous submissions
are not allowed) and sufficient detail to assess the merits and
relevance of the submission. Given the informal style of the
workshop, papers describing work in progress, with sufficient detail
to assess the contribution, are also welcome. Original papers should
not exceed 15 pages. 

* Extended abstracts: contain preliminary reports of work in progress,
case studies, or tool descriptions. These will be judged based on
the expected level of interest for the WING community. They will be
included in the CEUR-WS proceedings. Extended abstracts should not
exceed 5 pages. 

All submissions should conform to Springer's LNCS format. Formatting style 
files can be found at 

 http://www.springer.de/comp/lncs/authors.html 

Technical details may be included in an appendix to be read at the reviewers' 
discretion and to be omitted in the final version.

Please prepare your submission in accordance with the rules described above and 
submit a pdf file via

 https://www.easychair.org/?conf=wing2012


Publication
-----------

All submissions will be peer-reviewed by the program committee.
Accepted contributions will be published in archived electronic notes,
as a volume of CEUR Workshop Proceedings.

A special issue of the Journal of Science of Computer Programming with
extended versions of selected papers will be published after the workshop.


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.