G. Barthe, B. Gregoire, 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.
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.
Lilian Burdy, Marieke Huisman and Mariela Pavlova.
Preliminary Design of BML: A Behavioral Interface Specification
Language for Java bytecode. In
Fundamental Approaches to Software Engineering (FASE 2007),
pages 215-229. Volume 4422 of Lecture Notes in Computer Science,
Springer-Verlag, 2007.
Available from the URL ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/bml.pdf
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.
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.
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.
Gary T. Leavens.
JML's Rich, Inherited Specifications for Behavioral Subtypes.
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
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.
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.
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.
Tim Lindholm and Frank Yellin.
Java^TM Virtual Machine Specification, Second Edition.
Sun Microsystems, Inc., 1999.
http://java.sun.com/docs/books/vmspec/.
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.
Sun Microsystems, Inc.
Inner Classes Specification.
A part of the JDK^TM 1.1.8 Documentation, available from URL http://java.sun.com/products/archive/j2se-eol.html,
located in the directory docs/guide/innerclasses/