Boogie
Build Status, Linux, Windows, -------------------------------, ---------------------------------, ![linux build status][1], 
, [1]: https://travis-ci.com/boogie-org/boogie.svg?branch=master
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#.
For a sample verifier for a toy language built on top of Boogie, see
Forro.
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
Installation
Boogie releases are packaged as a .NET Core global tool available at
nuget.org. To install Boogie simply
run:
$ dotnet tool install --global boogie
To run Boogie, a supported SMT solver has to be available (see below).
Building
The preferred way to build (and run) Boogie today is using .NET Core.
Historically, Boogie can also be built using the classic .NET Framework (on
Windows) and Mono (on Linux/OSX), but this might not be supported in the future.
To run Boogie, a supported SMT solver has to be available (see below).
.NET Core
$ dotnet build Source/Boogie-NetCore.sln
The compiled Boogie binary is
Source/BoogieDriver/bin/${CONFIGURATION}/${FRAMEWORK}/BoogieDriver. Also, a
NuGet package is placed in Source/BoogieDriver/bin/Debug/ which can be used
for a local installation.
Windows (requires Visual Studio)
- Open
Source\Boogie.slnin Visual Studio. - Right click the
Boogiesolution in the Solution Explorer and clickRestore NuGet Packages. - Click
Build > Build Solution.
The compiled Boogie binary is Binaries\Boogie.exe.
Linux/OSX (requires Mono)
Either open Source\Boogie.sln in MonoDevelop and perform the same steps as
described for Visual Studio above, of compile on the command line as follows.
Fetch the NuGet packages that Boogie depends on:
$ nuget restore Source/Boogie.sln
Build Boogie:
$ msbuild Source/Boogie.sln
The compiled Boogie binary is Binaries/Boogie.exe, which can be executed with
mono or using the wrapper script Binaries/boogie.
Backend SMT Solver
The default SMT solver for Boogie is Z3.
Support for CVC4 and
Yices2 is experimental.
By default, Boogie looks for an executable called z3, cvc4, yices2[.exe] in your
PATH environment variable. If the solver executable is called differently on
your system, use /proverOpt:PROVER_NAME=<exeName>. Alternatively, an explicit
path can be given using /proverOpt:PROVER_PATH=<path>.
To learn how custom options can be supplied to the SMT solver (and more), call
Boogie with /proverHelp.
Z3
The current test suite assumes version 4.8.7, but earlier and newer versions may
also work.
CVC4 (experimental)
Call Boogie with /proverOpt:SOLVER=CVC4.
Yices2 (experimental)
Call Boogie with /proverOpt:SOLVER=Yices2 /useArrayTheory.
Works for unquantified fragments, e.g. arrays + arithmetic + bitvectors. Does
not work for quantifiers, generalized arrays, datatypes.
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
Versioning and Release Automation
The https://github.com/boogie-org/boogie/blob/master/.github/workflows/main.yml workflow will create and push a new tag each time commits are pushed to the master branch (including PR merges). By default, the created tag increments the patch version number from the previous tag. For example, if the last tagged commit were v2.4.3, then pushing to master would tag the latest commit with v2.4.4. If incrementing minor or major number is desired instead of patch, simply add #minor or #major to the first line of the commit message. For instance:
Adding the next greatest feature. #minor
If the last tagged commit were v2.4.3, then pushing this commit would generate the tag v2.5.0.
For pull-request merges, if minor or major version increments are desired, the first line of the merge commit message can be changed to include #minor or #major.
Note that on each push to master, the following will happen:
- A travis build for
masteris triggered. - The GitHub workflow is also triggered.
- Once the workflow pushes a new tag
vX.Y.Z, another travis build forvX.Y.Zis triggered. - The travis build for
vX.Y.Zin Release configuration publishes releases to GitHub and NuGet.org.
License
Boogie is licensed under the MIT License (see LICENSE.txt).