[Please post - apologies for multiple copies.] Call for Participation -------------------------- 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/ News ---- - Early registration deadline: May 13, 2007. - 8 papers have been accepted for presentation at the workshop. - 4 invited speakers (including 1 speaker of Calculemus 2007) confirmed. 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) - jointly with Calculemus 2007 Reiner Hahnle (Chalmers University of Technology, Goteborg, Sweden) Deepak Kapur (University of New Mexico, USA) Andrei Voronkov (Manchester University, UK) 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 --------------- May 13, 2007: Early registration deadline June 25-26, 2007: WING 2007 in Hagenberg 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.