Yusuf's Thoughts

L06 - Boogie and Boostan

6 min read

Back to Program Verification Index | Previous: (y-05) SMT-LIB | Next: (y-07) Relational Semantics

Mental Model for Boogie and Boostan

  • Why a new language? Real languages (C, Java) are too messy to verify directly. We translate them into a “clean” intermediate language like Boogie.
  • Boogie is a verification-oriented language. It has things programmers want (types, procedures) but is designed to be easily turned into logic formulas.
  • Boostan is a tiny, formal fragment of Boogie that we use in class to define perfect mathematical rules for how code works.
  • Boogaloo is a tool that lets us “run” Boogie code even when it’s non-deterministic, helping us find bugs early.

Why not verify C or Python directly?

  1. Syntax Bloat: These languages have hundreds of features that are hard to formalize.
  2. Vague Semantics: The rules for C are often defined in hundreds of pages of English text, which can be ambiguous.
  3. Intermediate Power: By translating many languages (C, Java, C#) into one intermediate language (Boogie), we only have to build one verifier.

The Verification Pipeline

Modern verifiers follow a specific translation chain:

  1. Source Code (e.g., C, Java): Messy, complex, and hardware-specific.
  2. Intermediate Language (e.g., Boogie): Clean, mathematical, and focused on assertions/assumptions.
  3. SMT Solver (e.g., Z3): Receives the logic formulas and checks if an assertion violation is “satisfiable” (meaning a bug exists).

Boogie: The Verification Language

Developed by Rustan Leino at Microsoft Research, Boogie is used by tools like Ultimate Automizer and Dafny.

Key Features of Boogie

  • Procedures: Named blocks of code with inputs and outputs.
  • requires P: A precondition that must hold before calling the procedure.
  • ensures Q: A postcondition that the procedure promises to satisfy upon termination.
  • Assignments: x := x + 1.
  • Assumptions: assume x > 0. If this is false, the execution “stops” or is ignored.
  • Assertions: assert x > 0. This is a promise that must hold true.

Example Boogie Code

procedure Square(a: int) returns (square: int)
    requires a >= 0;    // Precondition
    ensures square >= a; // Postcondition
{
    square := a * a;
    if (square == 0) {
        assume {:print "a is zero"} true;
    } else {
        assume {:print "a = ", a} true;
    }
}

Tool: Boogaloo

Boogaloo is an interpreter and symbolic executor for Boogie. It allows you to explore the state space of your Boogie code before running a full proof tool.

Command Line Options

  • -o [n]: Control the total number of executions to explore.
  • -n [n]: Limit the number of executions per unique sequence of statements (prevents getting stuck in infinite loops).
  • -c=0: Turns off “concrete mode” (allows variables to take symbolic values instead of just simple constants).
  • -p [proc]: Specifies the entry procedure to begin execution.

💡 Intuition: Asserts vs. Assumes

…

  • assume P: The verifier can take it for granted that P is true. It is a filter that tells the verifier, “Only look at cases where P holds.” If P is false, the path is ignored.

Boostan: The Formal Fragment

Boostan is a simplified version of Boogie used for defining formal relational semantics.

🧠 Deep Dive: The Formal Grammar

A Boostan program is a sequence of commands :

  • Skip: skip (Does nothing)
  • Assignment: x := e (Update variable with expression )
  • Sequence: (Execute , then )
  • If-Then-Else: if (b) { c_1 } else { c_2 }
  • While Loop: while (b) { c }
  • Havoc: havoc x (Assign a non-deterministic value to )
  • Assume: assume b (Filter execution paths)
  • Assert: assert b (Verify a condition)

💡 The “Small Vocabulary” Approach

Why do we limit Boostan to only a few commands?

  1. Ease of Formalization: It’s much easier to write mathematical rules for 8 commands than for 800.
  2. Completeness: These few commands are actually Turing-complete! Any complex program (with for loops, switch statements, etc.) can be rewritten using just these basic building blocks.
  3. Orthogonality: Each command does exactly one thing, making the semantics “clean” and predictable.

Summary

  1. Intermediate Languages like Boogie simplify verification by providing clean semantics.
  2. Boogie is the industry standard for intermediate verification; Boostan is our teaching version.
  3. Procedures in Boogie allow us to modularize proofs.
  4. Assumes filter states, while Asserts check for bugs.
  5. Boogaloo helps us debug our Boogie programs before we run a full verifier.

Self-Check

  1. Why do verifiers translate C, Java, or C# into Boogie instead of working on the source directly?
  1. What is the operational difference between assume P and assert P in Boogie?
  1. List the commands of Boostan () and explain why such a small set is enough.
  1. What is havoc x, and why does verification need it?
  1. What does Boogaloo do and how does it complement a full verifier?

Back to Program Verification Index | Previous: (y-05) SMT-LIB | Next: (y-07) Relational Semantics | (y) Return to Notes | (y) Return to Home

Graph View

Backlinks