Boogie: A Modular Reusable Verifier for Object-Oriented Programs

Mike Barnett; Bor-Yuh Evan Chang; Robert DeLIne; Bart Jacobs; Rustan Leino

Boogie: A Modular Reusable Verifier for Object-Oriented Programs

Mike Barnett ,
Bor-Yuh Evan Chang ,
Robert DeLIne ,
Bart Jacobs ,
Rustan Leino

FMCO 2005 | November 2005

Published by Springer Berlin Heidelberg

Download BibTex

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.