Specification and Verification of Object-Oriented Software (Part 0) - Leino, Rustan (International Summer School Marktoberdorf, Marktoberdorf, Germany, 2008)
Contents Theory and techniques for building a basic program verifier for a language with references to dynamically allocated objects A specification style and encoding thereof