Microsoft Research Boogie

Boogie is an Intermediate Verification Language (IVL) for describing proof obligations to be discharged by a reasoning engine, typically an SMT solver. The language is especially suitable when the proof obligations arise in the context of programs with control flow and imperative state. The intermediate language is easy to target from source languages such as C# or C. Boogie is also a verification engine that takes the Boogie language as input, generates verification conditions (VCs) for the proof obligations, and passes the VCs to a reasoning engine. In the Boogie pipeline, there is room for various Boogie-to-Boogie transforms that either encode certain features (like parallelism) or make the checking more effective or efficient.

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.

Last edited Jan 28 at 9:11 AM by danliew, version 26