Reading about OO Verification

I've been going back to read up on OO verification, and I found a very well-written paper entitled, Modular Invariants for Layered Object Structures. Peter Muller and Gary Leavens are co-authors, which comes as no surprise.

The thing is, this was a very easy to read paper that covers a lot of things about Ownership and OO Verification that I had sort of picked up along the way, but had never seen described in a comprehensive way. I guess that's partially due to the fact that it's a journal article, although frankly kind of a crazy journal. This paper uses Universe types, an extension of Ownership types, to prove class invariants. It's very similar to the Boogie methodology, or any of the papers on JML and verification, but this one actually takes the time to explain "classical" OO verification, which motivates the use of ownership.

I should have definitely read this a while ago considering this is basically what my own work is based on, but I guess I had been avoiding Ownership types for a while.

If you are at CMU and you want to check it out, our library has electronic access: here.