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 |
| Type: | TechReport |
| Number: | MSR-TR-2008-79 |
| Pages: | 70 |
| Institution: | Microsoft Research |