@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}, urltopdf = {http://people.inf.ethz.ch/lehnerh/pm/publications/getpdf.php?bibname=Own&id=LeinoMueller04a.pdf} }