April 1st, 2012
April 22nd, 2012
final versions:
June 3rd, 2012
July 8th, 2012

The workshop will be held in Soda Hall, room 320.

Program is up and proceedings are now available.


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.


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.