Boogie

Build Status

Linux	Windows

About

Boogie is an intermediate verification language (IVL), intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for Dafny, Chalice, and Spec#. A previous version of the language was called BoogiePL. The current language (version 2) is currently known as just Boogie, which is also the name of the verification tool that takes Boogie programs as input.

Boogie is also the name of a tool. The tool accepts the Boogie language as input, optionally infers some invariants in the given Boogie program, and then generates verification conditions that are passed to an SMT solver. The default SMT solver is Z3.

The Boogie research project is being developed primarily in the RiSE group at Microsoft Research in Redmond. However, people at several other institutions make the open-source Boogie tool what it is.

More documentation can be found at http://boogie-docs.readthedocs.org/en/latest/ .

Language Reference

See Language reference.

Note: This is Boogie2 details many aspects of the Boogie IVL but is slightly out of date.

Getting help

We have a public mailing list for users of Boogie. You can also report issues on our issue tracker

Building

Requirements

• NuGet
• Z3 4.4.1 or CVC4 FIXME_VERSION (note CVC4 support is experimental)

Windows specific

• Visual Studio >= 2012

Linux/OSX specific

• Mono

Windows

1. Open Source\Boogie.sln in Visual Studio
2. Right click the Boogie solution in the Solution Explorer and click Enable NuGet Package Restore. You will probably get a prompt asking to confirm this. Choose Yes.
3. Click BUILD > Build Solution.

Linux/OSX

You first need to fetch the NuGet packages that Boogie depends on. If you're doing this on the command line run

$ cd /path/to/repository
$ wget https://nuget.org/nuget.exe
$ mono ./nuget.exe restore Source/Boogie.sln

Note if you're using MonoDevelop it has a NuGet plug-in which you can use to "restore" the packages needed by Boogie.

Note if you see an error message like the following

WARNING: Error: SendFailure (Error writing headers)
Unable to find version '2.6.3' of package 'NUnit.Runners'.

then you need to initialise Mono's certificate store by running

$ mozroots --import --sync

then you can build by running

$ xbuild Source/Boogie.sln

Finally make sure there is a symlink to Z3 in the Binaries directory (replace with cvc4 if using CVC4 instead).

$ ln -s /usr/bin/z3 Binaries/z3.exe

You're now ready to run Boogie!

Testing

Boogie has two forms of tests. Driver tests and unit tests

Driver tests

See the Driver test documentation

Unit tests

See the Unit test documentation