Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including one for the object-oriented .NET language Spec#, the HAVOC and vcc verifiers for C, the Dafny language and verifier, and the concurrent language Chalice. A previous version of the language was called BoogiePL; the new version of the language is Boogie 2.
In their geneses, Boogie and Spec# were developed hand in hand. For this reason, the name Boogie has been used to describe Spec#-related things. In particular, the Spec# static program verifier, which translates compiled Spec# programs (.NET bytecode) into Boogie, has been called Boogie. In fact, this bytecode translator is still part of the Boogie executable, so the Boogie tool accepts compiled Spec# programs (extensions .dll and .exe) in addition to Boogie programs (extension .bpl). Finally, Spec# uses an ownership-based discipline for handling object invariants. This discipline is known as the Boogie methodology, but it is tied only to Spec# and its bytecode translator, not to the Boogie verification language.
The Boogie research project is being developed primarily in the RiSE group at Microsoft Research in Redmond.
Downloads
You can download the Boogie tool as part of the Spec# download. That download also contains the Z3 SMT solver. To run the Boogie tool, you need a .NET virtual machine, which comes built in with modern versions of Windows but is also available on other platforms.
Papers
If you want to learn more about the Boogie language and tool, good places to start are the Boogie 2 language reference manual and the Boogie tool architectural overview.
There are also lots of papers available at the Spec# web site.
- Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric, Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers, in Computer Aided Verification (CAV '09), Springer Verlag, February 2009
- K. Rustan M. Leino, Michal Moskal, and Wolfram Schulte, Verification Condition Splitting, 2008
