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 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.
The Boogie research project is being developed primarily in the
RiSE group at
Microsoft Research in Redmond. However, people at several other institutions make the open-source Boogie tool what it is.
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.
Historical notes
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, but the Spec# verifier is nowadays a separate tool (built on Boogie) called SscBoogie. 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.
Related Projects
Boogie has proven to be a great platform on top of which to implement other verification systems. Here is a partial list of such projects. If you know of others that should appear here, please let us know!
- Havoc: a tool for checking systems software written in C.
- Poirot: a property checker for concurrent programs.
- Symdiff: a windiff that shows semantic differences!
- VCC: a tool that analyzes concurrent C programs.
- Verve: an operating system whose type safety has been verified.
