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.
 PDF file |
Details
| Type: | TechReport |
| Number: | MSR-TR-2008-79 |
| Pages: | 70 |
| Institution: | Microsoft Research |
©2009 Microsoft Corporation. All rights reserved.