Next: , Previous: Static Verification of BML Specifications, Up: Top


Bibliography

[Barthe-Gregoire-Kunz-Rezk06]
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.
[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.
[BurdyHP07]
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
[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. 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.
[Ledgard80]
Henry. F. Ledgard. A Human Engineered Variant of BNF. ACM SIGPLAN Notices, 15(10):57-62, October 1980.
[LehnerM07]
H. Lehner and P. Müller. Formal Translation of Bytecode into BoogiePL. In M. Huisman and F. Spoto, editors, BYTECODE'07. ENTCS, 2007.
[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.
[Mallo07]
Ovidio Mallo. A Translator from BML annotated Java Bytecode to BoogiePL. Master's Thesis, ETH Zurich, 2007.
[Pavlova07]
Mariela Pavlova. Java bytecode verification and its applications. PhD Thesis, INRIA Sophia Antipolis/University of Nice, 2007.
[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 URL
http://java.sun.com/products/archive/j2se-eol.html, located in the directory docs/guide/innerclasses/
[Suzuki06]
Alex Suzuki. Translation Java Bytecode to BoogiePL. Master's Thesis, ETH Zurich, 2006.