BoogiePL: A typed procedural language for checking object-oriented programs

Robert DeLine and K. Rustan M. Leino

Abstract

This note defines BoogiePL, an intermediate language for program analysis and program verification. The language is a simple coarsely typed imperative language with procedures and arrays, plus support for introducing mathematical functions and declaring properties of these functions. BoogiePL can be used to represent programs written in an imperative source language (like an object-oriented .NET language), along with a logical encoding of the semantics of such a source language. From the resulting BoogiePL program, one can then generate verification conditions or perform other program analyses such as the inference of program invariants. In this way, BoogiePL also serves as a programming-notation front end to theorem provers. BoogiePL is accepted as input to Boogie, the Spec# static program verifier.

Details

Publication typeTechReport
NumberMSR-TR-2005-70
Pages13
InstitutionMicrosoft Research
> Publications > BoogiePL: A typed procedural language for checking object-oriented programs