Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 1st CFP: Workshop on Invariant Generation (WIN...


view this post on Zulip Email Gateway (Aug 18 2022 at 10:06):

From: Laura Kovacs <lkovacs@risc.uni-linz.ac.at>
[Please post - apologies for multiple copies.]

First 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 algebraic 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 algebraic 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)
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 (Standford University and Microsoft Research, 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/WING07/

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
(under negotiation).


Last updated: May 03 2024 at 08:18 UTC