Boogie is an intermediate verification language (IVL) at the heart of a large
verification ecosystem. The various frontends and backends for Boogie that participate in this ecosystem
rely on agreeing on the meaning of a given Boogie program. Despite this, Boogie does
not have a formal semantics. In this paper, we define a formal semantics for the
core of the Boogie IVL using the $\mathbb{K}$ framework. This work is also, to
the best of our knowledge, the first time a verification language has been
formalized using the semantics-first approach.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
