Email Gateway (Aug 18 2022 at 10:31): Email Gateway (Aug 18 2022 at 10:31):From: Laura Kovacs <lkovacs@risc.uni-linz.ac.at>
[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:
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.
Last updated: May 03 2024 at 08:18 UTC