University of Illinois Urbana-Champaign

KBoogie: A Formal Semantics for Boogie

Rodrigues, Nishant; Poulsen, Seth; Rosu, Grigore

Content Files
rodrigues-poulsen-rosu-2021-pldi-submission.pdf

Permalink

https://hdl.handle.net/2142/121901

Description

Title
KBoogie: A Formal Semantics for Boogie
Author(s)
  • Rodrigues, Nishant
  • Poulsen, Seth
  • Rosu, Grigore
Issue Date
2021-12-01
Keyword(s)
  • formal semantics
  • intermediate verification language
Date of Ingest
2024-02-24T16:51:29-06:00
Abstract
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.
Type of Resource
text
Genre of Resource
technical report
Language
eng

Owning Collections

Research and Tech Reports - Computer Science PRIMARY