The workshop will be held in Soda Hall, room 320.
Program is up and proceedings are now available.
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.
Submission
We welcome submissions up to 12 pages.
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.
Papers should be submitted through
EasyChair.
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)
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
Workshop Program
09:00
Emina Torlak: Toward a Shared Infrastructure for Code Checking, Angelic Execution, Debugging, and Synthesis (Invited Talk)
10:00
Coffee break
10:30
Jean-Christophe Filliâtre: Combining Interactive and Automated Theorem Proving using Why3 (Invited Tutorial)
12:00
Lunch break
1:30
Pierre-Emmanuel Cornilleau: Prototyping Static Analysis Certification using Why3
2:00
Guodong Li, Indradeep Ghosh, Sreeranga P. Rajan: KIL: An Abstract Intermediate Language for Symbolic Execution and Test Generation of C++ Programs
2:30
Francesco Alberti, Natasha Sharygina: Invariant Generation by Infinite-State Model Checking
3:00
Coffee break
3:30
Open Discussion: Software Verification Competition
17:30
The end
