For modular verification of programs involving mutable pointer structures and extensible classes, we need encapsulation for the portion of heap on which an object invariant depends. But what are dependence and encapsulation, and how can they be checked? Ownership type systems offer an answer in which encapsulation has static structure: ownership is not transferrable. Separation logic offers more flexible means to express ownership for fixed-size cells but has yet to be connected with extensible objects much less the class construct. This talk will survey some of the difficulties and recent accomplishments.

Joint work with Anindya Banerjee (Kansas State, USA), Peter Mueller (ETH Zurich) and Rustan Leino et al, Microsoft Research, Redmond