Boogie is a modeling language, 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, Spec#, and Move. For a sample verifier for a toy language built on top of Boogie, see Forro.
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.
Boogie has long been used for modeling and verifying sequential programs. Recently, through its Civl extension, Boogie has become capable of modeling concurrent and distributed systems.
Here are some resources to learn more about Boogie. Be aware that some information might be incomplete or outdated.
You can ask questions and report issues on our issue tracker.
We are happy to receive contributions via pull requests.
Boogie requires .NET Core and a supported SMT solver (see below).
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 build Boogie run:
$ dotnet build Source/Boogie.sln
The compiled Boogie binary is
Source/BoogieDriver/bin/${CONFIGURATION}/${FRAMEWORK}/BoogieDriver.
The default SMT solver for Boogie is Z3. Support for CVC5 and Yices2 is experimental.
By default, Boogie looks for an executable called z3|cvc5|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.
The current test suite assumes version 4.8.8, but earlier and newer versions may also work.
Call Boogie with /proverOpt:SOLVER=CVC5.
Call Boogie with /proverOpt:SOLVER=Yices2.
Works for unquantified fragments, e.g. arrays + arithmetic + bitvectors. Does not work for quantifiers, generalized arrays, datatypes.
Boogie has two forms of tests. Driver tests and unit tests
See the Driver test documentation
See the Unit test documentation
The current version of Boogie is noted in a build property. To push a new version to nuget, perform the following steps:
- Update the version (e.g., x.y.z) in
Source/Directory.Build.props git add Source/Directory.Build.props; git commit -m "Release version x.y.z"to commit the change locallygit push origin master:release-vx.y.zto push your change in a separate branch, whereoriginnormally denotes the remote on git.luolix.top- Create a pull request and wait for it to be approved and merged
git tag vx.y.zto create a local tag for the versiongit push origin vx.y.zto push the tag once the pull request is merged
The CI workflow will build and push the packages.
Boogie is licensed under the MIT License (see LICENSE.txt).