Bibliography

[Barthe-Gregoire-Kunz-Rezk06]

G. Barthe, B. Gr~goire, C. Kunz, and T. Rezk. Certificate translation for optimizing compilers. In Proceedings of the 13th International Static Analysis Symposium (SAS), LNCS, Seoul, Korea, August 2006. Springer-Verlag.

[Burdy-etal03]

Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An Overview of JML Tools and Applications, International Journal on Software Tools for Technology Transfer, February, 2005. A draft of this paper is also available via the JML website: ftp://ftp.cs.iastate.edu/pub/leavens/JML/jml-white-paper.pdf.

[Courbot-Pavlova-Grimaud-Vandewalle06]

A. Courbot, M. Pavlova, G. Grimaud and J-J. Vandewalle, A Low-Footprint Java-to-Native Compilation Scheme Using Formal Methods, In CARDIS 2006, pages 329-344, 2006.

[DeLine-Leino05]

R. DeLine and K. R. M. Leino, BoogiePL: A Typed Procedural Language for Checking Object-Oriented Programs, Technical Report MSR-TR-2005-70, Microsoft Research, 2005.

[Dietl-Mueller05]

Werner Dietl and Peter M~ller. Universes: Lightweight Ownership for JML. Journal of Object Technology, 4(8):5–32, October 2005. Available from http://www.jot.fm/issues/issue_2005_10/article1.pdf

[Dhara-Leavens96]

Krishna Kishore Dhara and Gary T. Leavens. Forcing Behavioral Subtyping Through Specification Inheritance. In Proceedings 18th International Conference on Software Engineering, Berlin, Germany, pages 258-267. IEEE 1996. An extended version is Department of Computer Science, Iowa State University, TR #95-20b, December 1995, which is available from the URL
ftp://ftp.cs.iastate.edu/pub/techreports/TR95-20/TR.ps.Z.

[Leavens06b]

Gary T. Leavens. JML's Rich, Inherited Specifications for Behavioral Subtypes. To appear in in Zhiming Liu and He Jifeng (eds), Proceedings, International Conference on Formal Engineering Methods (ICFEM'06), Macao, China, pages 2-36. Volume 4260 of Lecture Notes in Computer Science, Springer-Verlag, 2006. Also Department of Computer Science, Iowa State University, TR \#06-22, August 2006.
ftp://ftp.cs.iastate.edu/pub/techreports/TR06-22/TR.pdf

[Leavens-Baker-Ruby99]

Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: a Notation for Detailed Design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications for Businesses and Systems, chapter 12, pages 175-188.

[Leavens-Baker-Ruby06]

Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. ACM SIGSOFT Software Engineering Notes, 31(3):1-38, March 2006.
http://doi.acm.org/10.1145/1127878.1127884. Also Iowa State University, Department of Computer Science, TR #98-06-rev29, January 2006, which is available from the URL
ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.pdf.

[Leavens-Naumann06]

Gary T. Leavens and David A. Naumann. Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. Department of Computer Science, TR \#06-20a, July 2006, revised August 2006. Available from the URL
ftp://ftp.cs.iastate.edu/pub/techreports/TR90-09/TR.pdf.

[Lindholm-Yellin]

Tim Lindholm and Frank Yellin. Java^TM Virtual Machine Specification, Second Edition. Sun Microsystems, Inc., 1999. http://java.sun.com/docs/books/vmspec/.

[Quigley04]

C.L. Quigley. A Programming Logic for Java Bytecode Programs. PhD thesis, University of Glasgow, 2004.

[Raghavan-Leavens05]

Arun D. Raghavan and Gary T. Leavens. Desugaring JML Method Specifications. Technical Report 00-03a, Department of Computer Science, Iowa State University, Ames, Iowa, 50011, April, 2000, revised May 2005. Available in
ftp://ftp.cs.iastate.edu/pub/techreports/TR00-03/TR.ps.gz.

[InnerClasses-Sun97]

Sun Microsystems, Inc. Inner Classes Specification. A part of the JDK^TM 1.1.8 Documentation, available from http://java.sun.com/products/archive/j2se-eol.html, located in the directory docs/guide/innerclasses/