Boogie is an intermediate verification language and verification condition generator developed by Microsoft Research. Originally, part of the Spec# project though it has taken on a life of its own.

Notes related to Boogie verifier

Auto active verification, CIVL verifier, Corral verifier, Intermediate verification language, SMACK verifier, Spec# project, VCC verifier, Verification condition generator

Papers related to Boogie verifier

• Verifying constant-time implementations [almeida:security:2016]
• Verifying Rust programs with SMACK [baranowski:atva:2018]
• Specification and verification: The Spec# experience [barnett:cacm:2011]
• Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
• The Boogie verification debugger [legoues:sefm:2011]
• Developing verified programs with Dafny [leino:icse:2013]
• Dafny: An automatic program verifier for functional correctness [leino:lpair:2010]
• A polymorphic intermediate verification language: Design and logical encoding [leino:tacas:2010]
• SMACK: Decoupling source language details from verifier implementations [rakamaric:cav:2014]