HOL-Boogie — An Interactive Prover for the Boogie (2009)
Sascha Böhme, K. Rustan, M. Leino, Burkhart Wolff
Abstract Boogie is a program verification condition generator for an imperative core language. It has front-ends for the programming languages C # and C enriched by annotations in first-order logic....