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.
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.
- Mike Barnett and K. Rustan M. Leino, To Goto Where No Statement Has Gone Before, in VSTTE 2010, August 2010
- 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, This is Boogie 2, 24 June 2008
- K. Rustan M. Leino, Michal Moskal, and Wolfram Schulte, Verification Condition Splitting, Microsoft Research, 2008
- Mike Barnett and K. Rustan M. Leino, Weakest-precondition of unstructured programs, in PASTE '05: The 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, ACM Press, New York, NY, USA, 2005
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.
