Microsoft Research
Microsoft Translator |
Boogie Meets Regions: a Verification Experience Report (extended version)

Anindya Banerjee, Mike Barnett, and David A. Naumann
May 2008

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.

tr-2008-79.pdf
PDF file

Details

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