Add initial README.md

1 files changed, 105 insertions, 0 deletions

diff --git a/README.md b/README.md
new file mode 100644
index 00000000..ac4c12b1
--- /dev/null
+++ b/README.md
@@ -0,0 +1,105 @@
+# Boogie
+
+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.
+
+![boogie architecture](http://research.microsoft.com/en-us/projects/boogie/boogie.png)
+
+## Language Reference
+
+[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.3.2 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION**
+
+#### 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 ``cvc`` 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)