[Om-announce] CFP: BOOGIE 2012 - 2nd International Workshop on Intermediate Verification Languages

[Zvonimir Rakamaric]

**********************************************************************
CALL FOR PAPERS
**********************************************************************
BOOGIE 2012: 2nd Intl. Workshop on Intermediate Verification Languages
Co-located with CAV 2012
Berkeley, California, USA
July 8th, 2012
http://www.zvonimir.info/boogie2012/
**********************************************************************

*** IMPORTANT DATES ***

Submissions: April 1st, 2012
Notifications: April 22nd, 2012
Final versions: June 3rd, 2012
Workshop: July 8th, 2012


*** GOALS ***

An intermediate verification language (IVL), like Boogie or Why, is
used as a stepping stone between a source language and a reasoning
engine. IVLs promote modularization and sharing of infrastructure. For
example, the same IVL can have multiple source language front-ends and
multiple reasoning engine back-ends, forming a verification tool bus.
The goal of the Boogie Workshop is to advance theory and techniques
supporting IVLs, to bring together researchers working with IVLs, and
to promote sharing of infrastructure that they build.

The workshop is intended for topics related to any intermediate
verification language, not just Boogie.


*** MOTIVATION ***

There are several workshops that focus on specification features and
their encodings, as seen from the perspective of the end-user of the
verification tool (SAVCBS and FTFJP). On the other side of the
tool-chain are workshops that focus on decision procedures (SMT). The
Boogie Workshop is intended to fit in between, just like an
intermediate verification language sits between a source language and
an underlying reasoning engine.


*** TOPICS ***

- IVL tools
- language features of an IVL (e.g., angelic choice, tressa)
- type systems for an IVL
- translation from a source language to an IVL
- property inference at the level of an IVL (e.g., predicate
abstraction, abstract interpretation, termination metric inference,
Houdini-style inference)
- IVL to IVL translations (e.g., optimizations, slicing, translation
between different IVLs)
- translation from an IVL to reasoning engine (SMT, ATP, HOL) input
- interaction with reasoning engines
- interpretation of reasoning engine output in terms of the source
language via an IVL
- symbolic execution for an IVL
- axiomatizations of useful theories (like sets, sequences, heaps, ...)
- user experience improvements (e.g., caching of verification results)
- novel uses of IVLs (e.g., refinement or symbol diff)
- experimental evaluations (e.g., comparing different logical encoding
or reasoning engines)


*** SUBMISSION ***

We welcome submissions up to 12 pages in EPTCS format
[http://style.eptcs.org/]. The accepted papers will be printed in
informal proceedings distributed to the participants of the workshop.
With the exception of survey and history papers, the papers should
contain original work which has not been submitted or accepted for
publication elsewhere. We are planning to publish a selected subset of
the submitted papers as post-proceedings in a special volume of the
Electronic Proceedings in Theoretical Computer Science (EPTCS)
[http://eptcs.org/].

Papers should be submitted through EasyChair
[https://www.easychair.org/conferences/?conf=boogie2012].


*** PROGRAM COMMITTEE ***

Dino Distefano, Queen Mary University of London
Jean-Christophe Filliâtre, CNRS
Michał Moskal, Microsoft Research
Peter Müller, ETH
Shaz Qadeer, Microsoft Research
Zvonimir Rakamarić, University of Utah (Chair)
Stephen Siegel, University of Delaware
Ofer Strichman, Technion
Thomas Wies, New York University
Jochen Hoenicke, University of Freiburg

**********************************************************************