![\"\"](\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/boogie-boogie.png\")
<\/span><\/span>Boogie is also the name of a tool<\/b>. 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 (opens in new tab)<\/span><\/a>.\u00a0<\/span><\/span><\/div>\n- \n
- Try Boogie in your browser (opens in new tab)<\/span><\/a>!<\/li>\n
- Download (opens in new tab)<\/span><\/a>\u00a0Boogie.<\/li>\n
- Contribute to Boogie’s source code (opens in new tab)<\/span><\/a>.<\/li>\n<\/ul>\n
Papers<\/h2>\n
If you want to learn more<\/b> about the Boogie language and tool, good places to start are the\u00a0Boogie 2 language reference manual and the Boogie tool architectural overview.<\/p>\n
Historical notes<\/h2>\n
In their geneses, Boogie<\/b> and Spec# <\/b>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<\/b>, but it is tied only to Spec# and its bytecode translator, not to the Boogie verification language.<\/p>\n<\/div>\n
\nRelated Projects<\/h1>\n
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!<\/p>\n
- \n
- Havoc<\/a>: a tool for checking systems software written in C.<\/li>\n
- Poirot: a property checker for concurrent programs.<\/li>\n
- Symdiff<\/a>: a windiff that shows semantic differences!<\/li>\n
- VCC<\/a>: a tool that analyzes concurrent C programs.<\/li>\n
- Verve<\/a>: an operating system whose type safety has been verified.<\/li>\n<\/ul>\n<\/div>\n","protected":false},"excerpt":{"rendered":"
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 […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13561,13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-170118","msr-project","type-msr-project","status-publish","hentry","msr-research-area-algorithms","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2008-12-10","related-publications":[159550,157365,342743,155813,153732],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Akash Lal","user_id":30905,"people_section":"Group 1","alias":"akashl"},{"type":"user_nicename","display_name":"Shuvendu Lahiri","user_id":33640,"people_section":"Group 1","alias":"shuvendu"}],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170118","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":4,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170118\/revisions"}],"predecessor-version":[{"id":604440,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170118\/revisions\/604440"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170118"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170118"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170118"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170118"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170118"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
- Download (opens in new tab)<\/span><\/a>\u00a0Boogie.<\/li>\n