The Coq mailing list

[Laura Kovacs <lkovacs AT risc.uni-linz.ac.at>]

[Please post - apologies for multiple copies.]


Second Call for Papers

--------------------------
W I N G   2007

1st International Workshop on INvariant Generation
--------------------------

Research Institute for Symbolic Computation (RISC)
Johannes Kepler University
Hagenberg, Austria

June 25-26, 2007
Satellite Workshop of CALCULEMUS 2007 
in the frame of the RISC Summer 2007 conference series


http://www.risc.uni-linz.ac.at/about/conferences/WING2007/


General 
------- 
The increasing power of automated theorem proving 
and computer algebra have 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 the 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.

Program verification has a long research tradition but, 
so far, has had relatively little impact on practical 
software development in industry. However, the design 
and implementation of reliable software still is an 
important issue and any progress in this area will be 
of utmost importance for the future development of 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 the automated discovery of inductive 
assertions, leading to the discovery of safety and 
security properties of programs.


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

John Harrison (Intel Corporation, USA)
Reiner Hahnle (Chalmers University of Technology, Goteborg, Sweden) 
Deepak Kapur  (University of New Mexico, USA)




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

General Chair: 
Bruno Buchberger (RISC, Austria)

Program Chairs:
Tudor Jebelean (RISC, Austria)
Martin Giese (RISC, Austria)

Local Chair: 
Laura Kovacs (RISC, Austria)

Program Committee:
Nikolaj S. Bjorner (Stanford University and Microsoft Research, USA)
Ewen Denney (NASA Ames Research Center, USA)
Jens Knoop (Technical University of Vienna, Austria)
Enric Rodriguez Carbonell (Technical University of Catalonia, Barcelona, 
Spain)
Wolfgang Schreiner (RISC, Austria)
Helmut Seidl (Technical University of Munich, Germany)
Andrei Voronkov (Manchester University, UK)



Important Dates
---------------
February 26, 2007: Submission Deadline
April 25, 2007: Notification of Acceptance 
May 25, 2007:  Camera ready copy
June 25-26, 2007: WING 2007 in Hagenberg


Submission 
---------- 
Please submit your full paper of at most 12 pages prepared with
the standard LNCS class style as pdf or ps file via

  http://www.easychair.org/WING2007/

on or before February 26, 2007. 
Detailed formating instructions can be found on the WING website.


Proceedings
-----------

The accepted papers will be distributed to the participants 
as a working proceedings booklet (technical report).

The post-workshop proceedings volume will be published as a 
special issue of the  Journal of Symbolic Computation.