Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Boogie Meets Regions: a Verification Experience Report (extended version)

Anindya Banerjee, Mike Barnett, and David A. Naumann

Abstract

We use region logic specifications to verify several programs exhbiting the classic hard problem for object-oriented systems: the framing of heap updates. We use BoogiePL and its associated SMT solver, Z3, to prove both implementations and client code.

Details

Publication typeTechReport
NumberMSR-TR-2008-79
Pages70
InstitutionMicrosoft Research
> Publications > Boogie Meets Regions: a Verification Experience Report (extended version)