[Hol-info] 2nd CFP - Workshop on Invariant Generation (WING 2010), Edinburgh, July 21, 2010

[Laura K. <lk...@co...>]

[Please post - apologies for multiple copies.]


Second Call for Papers

--------------------------
W I N G 2010

3nd International Workshop on INvariant Generation
--------------------------

July 21, 2010
University of Edinburgh, UK
Satellite Workshop of FLoC 2010

http://research.microsoft.com/en-us/events/wing2010/




General
-------

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, the application areas are 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



Keynote Speakers
----------------

Sumit Gulwani (Microsoft Research, US)
Helmut Seidl  (Technical University of Munich, Germany)



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

Program Chairs:

Nikolaj Bjorner (Microsoft Research, US)
Laura Kovacs (Vienna University of Technology, Austria)


Program Committee:
Enric Rodríguez Carbonell (Technical University of Catalonia, Spain)
Martin Giese (University of Oslo, Norway)
Jens  Knoop (Vienna University of Technology, Austria)
Francesco Logozzo (Microsoft Research, USA)
Wolfgang Schreiner (RISC-Linz, Austria)
Andrey Rybalchenko (Technical University of Munich, Germany)
Helmut Veith (Vienna University of Technology, Austria)
Thomas Wies (IST, Austria)



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

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


Submission
----------

Submission is via EasyChair:

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


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 program 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.