Although binaries for Z3 are available for multiple platforms, installing Boogie on platforms other than Windows requires one to build Boogie from the source. However, some researchers use Linux or OSX as their development platform. Unfortunately, due to various issues, compiling from scratch can be a time-consuming endeavor. Boogie+Z3 is a convenience project aimed at busy researchers. We provide binary builds for OSX and Linux which integrate Boogie and Z3 into one neat package.
This package is a pre-built binary package for various platforms. We specifically support OSX 10.6+ and the latest stable release of Ubuntu Linux. It has been tested on OSX 10.6.7 and OSX 10.8 as well as Ubuntu Linux 12.10. It provides a working installation of Boogie and Z3 together. Unless otherwise stated, all builds require Mono 2.10.5 or later. You can download Mono from it’s project site, here: http://www.go-mono.com/mono-downloads/download.html
To install, simply download one of the provided binaries (over on the right). Then, copy the included boogie+z3 folder to "Applications" on OSX, or to the “opt” directory on Linux. From there you can run Boogie as follows:
# mono /Applications/boogie+z3/Binaries/Boogie.exe input.bpl
If you'd like to execute a shorter version of this command, create an alias like so:
# alias boogie='mono /Applications/boogie+z3/Binaries/Boogie.exe'
Boogie+Z3 includes a build script that enables you to build a package like the ones we release with minimal effort. The sections below detail the process of creating your own build. To begin, you should first check out the source of Boogie+Z3.
In the directory that contains this README file, note the two directories z3, and boogie. These are working checkouts of the Boogie and Z3 projects. Boogie is managed by mercurial and Z3 is managed by GIT. You can see which version is used in the build (or update the version) by performing the corresponding HG/GIT commands in those directories. The platform specific directories contain pre-build binaries for various platforms.
Platforms supported are MacOS X 10.6 and later and any Linux distribution that can run the Mono framework. Consequently, the Mono framework is required to build this package. On recent versions of Ubuntu Linux you can install Mono with the following command:
If you'd like to execute a shorter version of this command, create an alias like so:
# sudo apt-get install mono-complete
The other requirements you must satisfy are:
We do not distribute the source of Z3 and Boogie, but we provide a script that fetches the most current versions of them. If you want to use something other than the latest versions you will need to manually check them out. Note that the Boogie+Z3 script expects to see z3 and boogie in the “z3” and “boogie” directories, respectively.
To use the automatic script, run the command, below:
# sh fetch.sh
A Word of Warning: Because of a bug, checking out z3 on Linux (and some OSX systems) is non-trivial. Unless you have a really good reason for building from the source, you are better off using one of our builds.
To build Boogie+Z3, in the directory that contains this file, execute the following command:
# sh build.sh [platform]
Where platform is one of "OSX" or "LINUX."
Eg:
# sh build.sh LINUX
This will created the directory "dist" which will contain the binaries for your platform. The directory will be named boogie+z3. Copy the entire boogie+z3 directory to a location of your choosing.
Note: During the build process you will be prompted for your sudo password. Enter it and hit return.
To test:
# mono /path/to/boogie+z3/Binaries/Boogie.exe /path/to/boogie+z3/Test/AbsHoudini/f1.bpl
If you'd like to execute a shorter version of this command, create an alias like so:
# alias boogie='mono /path/to/boogie+z3/Binaries/Boogie.exe'
If you find this project useful or have any feedback I’d love to hear from you! You can reach me via the channels provided, below.
John L. Singleton
Email: jsinglet@gmail.com
Lab Homepage:
http://www.eecs.ucf.edu/~leavens/formal-methods-lab/people/john-l-singleton/
Personal Homepage: http://the-singleton.com