Boogie: A Modular Reusable Verifier for Object-Oriented Programs

  • Mike Barnett
  • Bor-Yuh Evan Chang
  • Bart Jacobs
  • Rustan Leino

FMCO 2005 |

Published by Springer Berlin Heidelberg

A program verifier is a complex system that uses compiler technology, program semantics, property inference, verification-condition generation, automatic decision procedures, and a user interface. This paper describes the architecture of a state-of-the-art program verifier for object-oriented programs.