Clone wiki

Boogaloo / Home



January 6, 2016: Boogaloo web interface has moved

October 21, 2013: Boogaloo is finally available with syntax highlighting from MSR's Rise4Fun!

October 16, 2013: Boogaloo is now used for teaching Boogie in the Software Verification course at ETH. Check out the lecture slides: pdf pptx

October 12, 2013: Check out the updated User Manual!

October 10, 2013: Boogaloo 0.4.3 released. It is a faster and more stable version of the symbolic Boogaloo powered by Z3. Available both for download and on the web.

May 30, 2013: The comcom web interface is now running the brand-new version of Boogaloo with symbolic execution and the Z3 constraint solver in the back-end. We will release this version and update the documentation below, once it becomes stable enough; for now you can check it out from the smt-constraints branch. Note that building it requires @wests 's version of z3-haskell.

February 5, 2013: Boogaloo 0.2 released, now with backtracking! Release notes

December 12, 2012: Try Boogaloo online! @haches created a simple web interface for Boogaloo, so now you can play around with the interpreter without downloading the executable. Thank you Christian!

October 30, 2012: The language-boogie package is now on Hackage

October 25, 2012: Boogaloo 0.1 released

What is Boogaloo?

Boogaloo is an interpreter and run-time assertion checker for the Boogie intermediate verification language. Usually Boogie programs do not get executed: they are meant to be proven correct by the Boogie verifier. When a verification attempt fails, however, it is often hard to understand what went wrong. Is the specification inconsistent with the program or just incomplete? On what inputs does the specification violation occur?

Boogaloo helps you understand failed verification attempts, debug Boogie programs and test translations from a source language into Boogie. It can try out a number of program executions and check if the specification holds in those cases, even if some loop invariants or intermediate assertions are missing. If a specification violation occurs, Boogaloo produces a concrete failing test case, which can help you figure out what the error is and how to fix it.

As an example, consider the following (erroneous) implementation of the Mc-Carthy 91 function:

1:  procedure F(n: int) returns (r: int)
2:    ensures n <= 100 ==> r == 91;
3:  {
4:    if (100 <= n) {
5:      r := n - 10;
6:    } else {
7:      call r := F(n + 11);
8:      call r := F(r);
9:    }
10: }

The Boogie verifier can only tell us that the postcondition might not hold. If instead you test this program with Boogaloo, like so:

boogaloo test McCarthy-91.bpl

it will produce the following output:

Execution 0: F(100) failed
Postcondition "n <= 100 ==> r == 91" defined at McCarthy-91.bpl line 2 
violated at McCarthy-91.bpl line 1 with
    n -> 100
    r -> 90
in call to F

The failing test case hints us at the problem: when F is invoked with n = 100, r comes out as 90 instead of 91. We can fix this by changing the first line of the body into if (100 < n) { . After this change verification still fails but all the tests pass, which indicates that the program is likely to be correct, just missing some specification (in this case, the second postcondition clause).

To check out what else Boogaloo can do try it on sample Boogie programs from the examples directory.

Further Reading