[isabelle] 2nd CFP: Workshop on Invariant Generation (WING 2007), RISC, Hagenberg, Austria, 25-26 June, 2007
[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
June 25-26, 2007
Satellite Workshop of CALCULEMUS 2007
in the frame of the RISC Summer 2007 conference series
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.
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
John Harrison (Intel Corporation, USA)
Reiner Hahnle (Chalmers University of Technology, Goteborg, Sweden)
Deepak Kapur (University of New Mexico, USA)
Bruno Buchberger (RISC, Austria)
Tudor Jebelean (RISC, Austria)
Martin Giese (RISC, Austria)
Laura Kovacs (RISC, Austria)
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)
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
Please submit your full paper of at most 12 pages prepared with
the standard LNCS class style as pdf or ps file via
on or before February 26, 2007.
Detailed formating instructions can be found on the WING website.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and