@TechReport{LeinoMueller04a, author = {Leino, K. R. M. and M\"uller, P.}, title = {Modular verification of global module invariants in object-oriented programs}, institution = {ETH Zurich}, year = {2004}, number = {459}, url = {www.inf.ethz.ch/research/publications/techreports/show?serial=459〈=en} }