Boogie Meets Regions: a Verification Experience Report (extended version)
- Anindya Banerjee ,
- Mike Barnett ,
- David A. Naumann
MSR-TR-2008-79 |
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.