blob: beb217fdf312e2822623c51edb128b6bcf57f876 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
# Boogie
## Build Status
| Linux | Windows |
|-------------------------------|---------------------------------|
| [![linux build status][1]][2] | [![windows_build_status][3]][4] |
[1]: https://travis-ci.org/boogie-org/boogie.svg?branch=master
[2]: https://travis-ci.org/boogie-org/boogie
[3]: https://pmbuilds.inf.ethz.ch/buildStatus/icon?job=boogie
[4]: #FIXME
## 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](https://github.com/Z3Prover/z3).
The Boogie research project is being developed primarily in the [RiSE
group](http://research.microsoft.com/rise) at [Microsoft
Research](http://research.microsoft.com/) 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](http://boogie-docs.readthedocs.org/en/latest/LangRef.html).
Note: [This is Boogie2](http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf) details
many aspects of the Boogie IVL but is slightly out of date.
## Getting help
We have a public [mailing list](https://mailman.ic.ac.uk/mailman/listinfo/boogie-dev) for users of Boogie.
You can also report issues on our [issue tracker](https://github.com/boogie-org/boogie/issues)
## Building
### Requirements
- [NuGet](https://www.nuget.org/)
- [Z3](https://github.com/Z3Prover/z3) 4.4.1 or [CVC4](http://cvc4.cs.nyu.edu/web/) **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](Test/README.md)
### Unit tests
See the [Unit test documentation](Source/UnitTests/README.md)
|
