Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 2nd CFP - Workshop on Invariant Generation (WI...


view this post on Zulip Email Gateway (Aug 18 2022 at 12:43):

From: Laura Kovacs <laura.kovacs@epfl.ch>
[Please post - apologies for multiple copies.]

Second Call for Papers


W I N G 2009

2nd International Workshop on INvariant Generation


March 22-23, 2009, University of York, UK
Satellite Workshop of ETAPS 2009

http://mtc.epfl.ch/events/WING09/

General


Program verification has a long research tradition, but so far
its impact on development of safety critical software has been
relatively limited. A key impediment has been the overhead
associated with providing and debugging auxiliary invariant
annotations. As the design and implementation of reliable
software remains an important issue, any progress in this area
will be of utmost importance for future developments in 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 automated discovery of inductive assertions,
leading to verification of safety and security properties of
programs.

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

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


Leonardo de Moura (Microsoft Research, USA)
Andrey Rybalchenko (MPI Saarbruecken, Germany)

Committee


Program Chairs:

Andrew Ireland (Heriot-Watt University, UK)
Laura Kovacs (EPFL, Switzerland)

Program Committee:

Nikolaj Bjorner (Microsoft Research, USA)
Martin Giese (University of Oslo, Norway)
Reiner Haehnle (Chalmers University of Technology, Sweden)
Paul Jackson (University of Edinburgh, UK)
Jens Knoop (Technical University of Vienna, Austria)
Francesco Logozzo (Microsoft Research, USA)
Wolfgang Schreiner (RISC-Linz, Austria)
Helmut Veith (Technical University of Darmstadt, Germany)
Andrei Voronkov (Manchester University, UK)
Thomas Wies (EPFL, Switzerland)

Important Dates


January 12, 2009: Submission deadline
February 16, 2009: Notification of acceptance
March 1, 2009: Camera-ready copy deadline
March 22-23, 2009: WING 2009 in York, UK

Submission


Submission is via

http://www.easychair.org/conferences/?conf=wing09

Please submit research reports up to 15 pages in PDF,
conforming to the format produced by LaTeX using the
easychair.cls class file of EasyChair.
The class style may be downloaded at:

http://www.easychair.org/easychair.zip

Publication


All submissions will be peer-reviewed by the programme committee.
Accepted contributions will be published in archived electronic notes,
as an EasyChair collection volume.

Journal publication of the post-workshop proceedings volume
is under discussion.


Last updated: Nov 21 2024 at 12:39 UTC