@inproceedings{LP-VSTTE2013, author = {K. Rustan M. Leino and Nadia Polikarpova}, title = {Verified Calculations}, booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE)}, year = {2013}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {8164}, urltopdf = {http://se.inf.ethz.ch/people/polikarpova/publications/vstte13.pdf} }