Microsoft Research Boogie

(aka The World's Best Program Verification System)
Boogie is a program verification system that produces verification conditions for programs written in an intermediate language (also named Boogie). The intermediate language is easy to target from source languages such as Spec#, C#, or even C.

• Frequently asked questions
• External Dependencies
• How to install the binaries
• How to install and build the sources
• How to install and build the sources using Mono (for OS X and Linux platforms)
• How to run the Boogie Verification Debugger
• How to contribute
• MSR Boogie site
• BOOGIE 2011: first international workshop on intermediate verification languages*

This project is sponsored by the Research in Software Engineering Group (RiSE) based in the Microsoft Research Redmond Laboratory.

Now you can try Boogie from your webbrowser at the RiSE4Fun website. The website also supports Dafny.