The Java Modeling Language (JML)

Papers Related to JML

The following papers are related to JML, but are also concerned with other matters (typically semantics of formal methods or tool support). They are listed in (approximately) reverse chronological order. Note that JML's syntax and semantics may be different from that used in older papers. You should consult the latest documentation for current details.

If you have a paper related to JML that does not appear here, we'd like to include it. If you are a developer on the sourceforge.net jmlspecs project, you can update the CVS for this web page by checking out the module named web and commiting changes to the papers.shtml file. Or, if you aren't a developer, or if that's too much trouble, just send a citation for your paper (in XHTML, please, with links for each author and a link to a PDF file) to Gary Leavens.

Bibtex entries for the papers on this page are available from the Collection of Computer Science Bibliographies or from Gary Leavens's bibliographies. If your paper's bibtex entry is inaccurate or not available from these sources, then please send it (in bibtex format!) to Gary Leavens.

• Patrice Chalin. A Sound Assertion Semantics for the Dependable Systems Evoluation Verifying Compiler. In ICSE 2007, May 2007, pages 23-33. [DOI: 10.1109/ICSE.2007.9]
  Also ENCS-CSE TR 2006-001 revision 4, February 2007.
• Patrice Chalin. Perry R. James, and George Karabotsos. The Architecture of JML4, a Proposed Integrated Verification Environment for JML. Dependable Software Research Group, Concordia University, ENCS-CSE-TR 2007-006. May, 2007. [PDF]
• Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova and Antoine Requet. JACK: a tool for validation of security and behaviour of Java applications. Formal Methods for Components and Objects (FMCO 2006). To appear, 2007.
• Jeremy Kirk. Software Project Aims to Secure E-Voting. PC World, April 16, 2007. [On-line article]
• Yoonsik Cheon and Ashaveena Perumandla. Specifying and Checking Method Call Sequences of Java Programs. Software Quality Journal, 15(1):7-25, March 2007. [DOI: 10.1007/s11219-006-9001-4]
  Also Department of Computer Science, The University of Texas at El Paso, TR #05-36, November 2005; revised April 2006. [PDF]
• Steve M. Shaner, Gary T. Leavens, David A. Naumann, Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs. To appear in OOPSLA 2007.
  Also Department of Computer Science, Iowa State University, TR #07-04b, March 2007, revised April, July 2007. [abstract] [PDF] [postscript]
• Tao Xie, Kunal Taneja, Shreyas Kale, and Darko Marinov. Towards a Framework for Differential Unit Testing of Object-Oriented Programs. To appear in Proceedings of the 2nd International Workshop on Automation of Software Test (AST 2007), Minneapolis, MN, May, 2007 [PDF]
• Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt (eds.). Verification of Object-Oriented Software: The KeY Approach. Volume 4334 of Lecture Notes in Computer Science, Springer-Verlag, 2007. (ISBN: 978-3-540-68977-5)
• Lilian Burdy, Marieke Huisman, and Mariela Pavlova. Preliminary Design of BML: A Behavioral Interface Specification Language for Java bytecode. Fundamental Approaches to Software Engineering (FASE 2007), 2007. [PDF]
• Erik Poll and Aleksy Schubert, Verifying an implementation of SSH. WITS, 2007. [PDF]
• Gary T. Leavens, David A. Naumann, and Stan Rosenberg. Preliminary Definition of Core JML. Stevens Institute of Technology, CS Report 2006-07, 2006. [PDF]
• Gary T. Leavens and David A. Naumann. Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs. Department of Computer Science, Iowa State University, TR #06-36, December 2006. [abstract] [PDF] [postscript]
• Clyde Dwain Ruby. Modular subclass verification: safely creating correct subclasses without superclass code. Department of Computer Science, Iowa State University, TR #06-34, December 2006. [abstract] [PDF]
• Joseph R. Kiniry, Alan E. Morkan, and Barry Denby. Soundness and Completeness Warnings in ESC/Java2. Fifth International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2006), pages 19-24, November 2006. [PDF]
• Patrice Chalin. Early Detection of JML Specification Errors using ESC/Java2. Fifth International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2006), pages 25-32, November 2006. [PDF]
• Julien Groslambert, Jacques Julliand, and Olga Kouchnarenko. JML-based Verification of Liveness Properties on a Class. Fifth International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2006), pages 41-48, November 2006. [PDF]
• David R. Cok. Specifying Java Iterators with JML and Esc/Java2. Fifth International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2006), pages 71-74, November 2006. [PDF]
• Gary T. Leavens and Peter Müller. Information Hiding and Visibility in Interface Specifications. In ICSE 2007, May 2007, pages 385-395. [DOI: 10.1109/ICSE.2007.44]
  Also Department of Computer Science, Iowa State University, TR #06-28, September 2006. [abstract] [Preprint PDF] [Preprint PostScript]
• Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Invariants for Layered Object Structures. Science of Computer Programming, 62(3):253-286, Elsevier, Oct. 2006. http://dx.doi.org/10.1016/j.scico.2006.03.001
  Also ETH Zurich, Technical Report 424, October 2003, revised March 2004, March 2005. [abstract] [Preprint PDF]
• Isabel Nunes, Antónia Lopes, Vasco Vasconcelos, João Abreu, and Luis S. Reis. Checking the Conformance of Java Classes Against Algebraic Specifications. In Zhiming Liu and He Jifeng (eds), Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM), Macao, China, pages 494-513. Volume 4260 of Lecture Notes in Computer Science, Springer-Verlag, 2006. [PDF]
• Leo Freitas, Ana Cavalcanti, and Jim Woodcock. Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking. In Zhiming Liu and He Jifeng (eds), Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM), Macao, China, pages 697-716. Volume 4260 of Lecture Notes in Computer Science, Springer-Verlag, 2006.
• Gary T. Leavens. JML's Rich, Inherited Specifications for Behavioral Subtypes. In Zhiming Liu and He Jifeng (eds), Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM), Macao, China, pages 2-34. Volume 4260 of Lecture Notes in Computer Science, Springer-Verlag, 2006.
  The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/11901433_2.
  [Powerpoint]
  Also Department of Computer Science, Iowa State University, TR #06-22, August 2006. [abstract] [postscript] [PDF]
• Gary T. Leavens and David A. Naumann. Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. Department of Computer Science, Iowa State University, TR #06-20b, July 2006, revised August, September 2006. [abstract] [postscript] [PDF]
• Ben Krause and Tim Wahls. jmle: A Tool for Executing JML Specifications via Constraint Programming. In L. Brim, editor, Formal Methods for Industrial Critical Systems (FMICS '06). Bonn, Germany. August 26-27, 2006. Volume 4346 of Lecture Notes in Computer Science, Springer Verlag, 2007, pages 293-296. [PDF]
• Cui Ye. Improving JML's assignable clause analysis. Department of Computer Science, Iowa State University, TR #06-19-23, July 2006. [abstract] [PDF]
• Mike Barnett, David A. Naumann, Wolfram Schulte, and Qi Sun. Allowing State Changes in Specifications. To appear in International Conference on Emerging Trends in Information and Communication Security (ETRICS), 2006. [PDF]
• David A. Naumann. From Coupling Relations to Mated Invariants for Secure Information Flow. To appear in European Symposium on Research in Computer Security (ESORICS), 2006. [PDF]
• David A. Naumann. Observational Purity and Encapsulation. To appear in Theoretical Computer Science, 2006. [PDF]
• Alexandre Courbot, Mariela Pavlova, Gilles Grimaud and Jean-Jacques Vandewalle. A Low-Footprint Java-to-Native Compilation Scheme Using Formal Methods. In CARDIS 2006, pages 329-344, 2006. [PDF]
• Lilian Burdy and Mariela Pavlova. Java Bytecode Specification and Verification. In SAC 2006, ACM, 2006. [PDF]
• Marcelo d'Amorim, Carlos Pacheco and Tao Xie, Darko Marinov, and Michael Ernst. An Empirical Comparison of Automated Generation and Classification Techniques for Object-Oriented Unit Testing. To appear in Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering (ASE 2006), Tokyo, Japan, September 2006. [PDF]
• Gary T. Leavens, K. Rustan M. Leino, and Peter Müller. Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing, 19(2):159-189, June 2007. The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/s00165-007-0026-7.
  Also Department of Computer Science, Iowa State University, TR #06-14a, May 2006, revised August 2006. [abstract] [PDF] [PostScript]
• Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. In Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures, pages 342-363. Volume 4111 of Lecture Notes in Computer Science, Springer Verlag, 2006.
  The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/11804192_16.
  [Corrected PDF]
• Christoph Csallner and Yannis Smaragdakis. DSD-Crasher: A hybrid analysis tool for bug finding. In Proceedings International Symposium on Software Testing and Analysis (ISSTA), pages 245-254. ACM, July 2006. [Abstract] [PDF]
• Robert Atkey. Specifying and Verifying Heap Space Allocation with JML and ESC/Java2 (Preliminary Report). In Formal Techniques for Java-Like Programs 2006, July 4, 2006. [PDF]
• Patrice Chalin. Towards Support for Non-null Types and Non-null-by-default in Java. In Formal Techniques for Java-Like Programs 2006, July 4, 2006. [PDF]
• Julien Charles. Adding native specifications to JML. In Formal Techniques for Java-Like Programs 2006, July 4, 2006. [PDF]
• Ádám Darvas and Peter Müller. Reasoning About Method Calls in Interface Specifications. Journal of Object Technoloby, special issue: ECOOP 2005 Workshop FTfJP, 5(5):59-85, June 2006, http://www.jot.fm/issues/issue_2006_06/article3. [PDF]
• Neeraj Khanolkar and Gary T. Leavens. Executable Documentation of Template-Hook Interactions in Frameworks using JML. Department of Computer Science, Iowa State University, TR #06-18, June 2006. [abstract] [postscript] [PDF]
• 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. [PDF]
• Christoph Csallner and Yannis Smaragdakis. Dynamically discovering likely interface invariants. In Proc. 28th International Conference on Software Engineering, Emerging Results Track, pages 861-864, May 2006. [Abstract] [PDF]
• Poonam Agarwal, Carlos E. Rubio-Medrano, Yoonsik Cheon, and Patricia J. Teller. Formal Specification in JML of the Java Security Package. Department of Computer Science, The University of Texas at El Paso, TR #06-13, April 2006. [PDF]
• Gary T. Leavens. Not a Number of Floating Point Problems. Journal of Object Technology, 5(2):75-83, March-April 2006, http://www.jot.fm/issues/issues_2006_03/column8.
• David A. Naumann. Observational Purity and Encapsulation. In Fundamental Aspects of Software Engineering (FASE), pages 190-204, 2005. Awarded Best Software Science Paper by the European Association of Software Sciences and Technology at the European Joint Conferences on Theory and Practice of Software (ETAPS) 2005. [PDF]
• Patrice Chalin and Frédéric Rioux. Non-null References by Default in the Java Modeling Language. In Proceedings of the Workshop on the Specification and Verification of Component-Based Systems (SAVCBS'05), Lisbon, Portugal, September, 2005. An updated version is ENCS-CSE TR 2005-004, December 2005.
• Yoonsik Cheon, Myoung Yee Kim, and Ashaveena Perumandla. A Complete Automation of Unit Testing for Java Programs. In Proceedings of the 2005 International Conference on Software Engineering Research and Experience (SERP '05), Las Vegas, Nevada, June 27-30, 2005, pages 290-295. Department of Computer Science, The University of Texas at El Paso, TR #05-05, February, revised July 2005. [PDF]
• Sophie Cupuy-Chessa, Lydie du Bousquet, Jullien Bouchet, and Yves Ledru. Test of the ICARE platform fusion mechanism. In Proceedings of DSVIS'05 - Int. Workshop on Design Specification and Verification of Interactive Systems, Newcastle, July 2005. Lecture Notes in Computer Science, Springer Verlag, 2005. [PDF] The original publication will be available at springerlink.com.
• Cees-Bart Breunesse, Néstor Cataño, Marieke Huisman, and Bart P.F. Jacobs. Formal Methods for Smart Cards: an experience report. Science of Computer Programming, 55(1-3):53-80, Elsevier, 2005. [PDF].
  An earlier version appeared as NIII report NIII-R0316, 2005.
• Catherine Oriat. Jartege: A Tool for Random Generation of Unit Tests for Java Classes. In R. Reusner, et al. (eds), Quality of Software Architectures and Software Quality First International Conference on the Quality of Software Architectures, QoSA 2005 and Second International Workshop on Software Quality, SOQUA 2005, Erfurt, Germany, September, 20-22, 2005, QoSA/SOQUA 2005, pages 242-256. Volume 3712 of Lecture Notes in Computer Science, Springer Verlag, 2005. ISBN 3-540-29033-8.
• Edwin Rodríguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby. Extending JML for Modular Specification and Verification of Multi-Threaded Programs. In Andrew P. Black (ed.), ECOOP 2005 -- Object-Oriented Programming 19th European Conference, Glasgow, UK, pages 551-576. Volume 3586 of Lecture Notes in Computer Science, Springer Verlag, July 2005. The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/11531142_24.
  Also Kansas State University, Department of Computing and Information Sciences, Technical Report, SAnToS-TR2004-10, December 2004, revised May 2005. [PDF]
• Carlos Pacheco and Michael Ernst. Eclat: Automatic generation and classification of test inputs. In Andrew P. Black (ed.), ECOOP 2005 -- Object-Oriented Programming 19th European Conference, Glasgow, UK, pages 504-527. Volume 3586 of Lecture Notes in Computer Science, Springer Verlag, July 2005. [PDF]
• Gary T. Leavens and Curtis Clifton. Lessons from the JML Project. To appear in Bertrand Meyer and Jim Woodcock (eds.), Verified Software: Theories, Tools, Experiments, Zürich, Switzerland, October, 2005. Springer-Verlag.
  Also Department of Computer Science, Iowa State University, TR #05-12a, April 2005, revised July 2005. [abstract] [PDF] [PostScript]
• Joseph Kiniry, Patrice Chalin, and Clément Hurlin. Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification. In Verified Software: Theories, Tools, Experiments, Zürich, Switzerland, October, 2005. [PDF]
• Peter Müller. Reasoning about Object Structures Using Ownership. In Verified Software: Theories, Tools, Experiments, Zürich, Switzerland, October, 2005. [PDF]
• Michael Möller. Mapping formal specifications to Java contracts. In Proceedings of the 17th Nordic Workshop on Programming Theory, pages 100-102. University of Copenhagen, Denmark, October 2005. [PDF]
• Gilles Barthe, Mariela Pavlova and Gerardo Schneider. Precise analysis of memory consumption using program logics. In Proceedings of the 3rd International Conference on Software Engineering and Formal Methods (SEFM'05), pages 86-95, Koblenz, Germany, September, 2005. [PDF]
• Patrice Chalin. Logical Foundations of Program Assertions: What do Practitioners Want? In Proceedings of the 3rd International Conference on Software Engineering and Formal Methods (SEFM'05), Koblenz, Germany, September, 2005. Also ENCS-CSE TR 2005-002.
• Ádám Darvas and Peter Müller. Reasoning About Method Calls in JML Specifications. Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP'05), Glasgow, Scotland, July, 2005. [PDF]
• Patrice Chalin. Reassessing JML’s Logical Foundation. In Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP'05), Glasgow, Scotland, July, 2005. Also ENCS-CSE TR 2005-005.
• F. Bouquet, F. Dadeau, B. Legeard and M. Utting. Symbolic Animation of JML Specifications. In Proceedings of the International Conference on Formal Methods 2005 (FM'05), pages 75-90. Volume 3582 of Lecture Notes in Computer Science, Springer Verlag, July 2005. 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, 7(3):212-232, June 2005. The original publication is available at http://www.springerlink.com from http://dx.doi.org/10.1007/s10009-004-0167-4.
  Preprint: [PDF]
• Tao Xie, Darko Marinov, Wolfram Schulte, and David Notkin. Symstra: A Framework for Generating Object-Oriented Unit Tests using Symbolic Execution. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Edinburgh, U.K., pp. 365-381, April 2005. [PDF]
• F. Bouquet, F. Dadeau, and J. Groslambert. Checking JML Specifications with B Machines. In Proceedings of the International Conference on Formal Specification and Development in Z and B (ZB'05), pages 435-454. Volume 3455 of Lecture Notes in Computer Science, Springer Verlag, April 2005. Springer-Verlag
• Gary T. Leavens, Yoonsik Cheon, and David R. Cok. Demonstration of JML Tools. Department of Computer Science, Iowa State University, TR #05-13, April 2005. [abstract] [PDF] [PostScript]
• Werner Dietl and Peter Müller. Universes: Lightweight Ownership for JML. In Journal of Object Technology, 4(8):5-32, 2005. http://www.jot.fm/issues/issue_2005_10/article1.
• F. Rioux and P. Chalin. Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study. In Proceedings of the 1st International Workshop on Automated Specification and Verification of Web Sites, Valencia, Spain, Electronic Notes in Theoretical Computer Science, March 14-15, 2005.
• Yoonsik Cheon, Gary T. Leavens, Murali Sitaraman, and Stephen Edwards. Model Variables: Cleanly Supporting Abstraction in Design By Contract. Software, Practice & Experience, 35(6):583-599, Wiley, May, 2005. http://dx.doi.org/10.1002/spe.649
  Also Department of Computer Science, Iowa State University, TR #03-10b, March 2003, revised September 2003, August 2004. [abstract] [PDF] [Postscript]
• Robby, Edwin Rodríguez, Matthew B. Dwyer, and John Hatcliff. Checking JML Specifications Using An Extensible Software Model Checking Framework. To appear in International Journal on Software Tools for Technology Transfer, 2006. Available at http://www.springerlink.com.
  An earlier version is Kansas State University, Department of Computer and Information Sciences, Technical Report, SAnToS-TR2004-7, May 2005 [PDF]
• Yoonsik Cheon and Gary T. Leavens. A Contextual Interpretation of Undefinedness for Runtime Assertion Checking. In AADEBUG 2005 Sixth International Symposium On Automated And Analysis-Driven Debugging, Monterey, California, September 2005, pages 149-158.
  Also Department of Computer Science, The University of Texas at El Paso, Technical Report #05-10, March 2005. [PDF]
• Kiyoshi Yamada and Takuo Watanabe. An Aspect-Oriented Approach to Modular Behavioral Specification of Java components. In IASTED Conf. on Software Engineering, pages 360-365, 2005.
• Kiyoshi Yamada and Takuo Watanabe. Moxa: An Aspect-Oriented Approach to Modular Behavioral Specifications. In SPLAT '05, March 2005. [PDF]
• Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming, 55(1-3):185-205, Elsevier, March, 2005. http://dx.doi.org/10.1016/j.scico.2004.05.015
  Preprint: Department of Computer Science, Iowa State University, TR #03-04a, revised March 2004. [abstract] [PDF]
• David R. Cok. Reasoning with specifications containing method calls and model fields. Journal of Object Technology, Special Issue: ECOOP 2004 Workshop FTfJP, 4(8):77-103, October 2005. http://www.jot.fm/issues/issue_2005_10/article4.
• Roy Patrick Tan and Stephen H. Edwards. Experiences evaluating the effectiveness of JML-JUnit testing, in Proceeedings of the 2004 Workshop on empirical research in software testing, 2004. (ACM SIGSOFT Software Engineering Notes, Volume 29, number 5, September 2004.) [PDF].
• F. Bellegarde, J. Groslambert, Marieke Huisman, O. Kouchnarenko, and J. Julliand. Verification of Liveness Properties with JML. INRIA Technical Report, nr. RR-5331, 2004. [Postscript]
• M. Pavlova, G. Barthe, L. Burdy, Marieke Huisman, J.-L. Lanet. Enforcing High-Level Security Properties For Applets. In J.-J. Quisquater, P. Paradinas, Y. Deswarte, and A.A. El Kalam (eds.), CARDIS'04, pages 1--16. Kluwer. [PDF]
  An earlier version appeared as INRIA Technical Report, nr. RR-5061, 2004
• Y. Ledru, Lydie du Bousquet, Olivier Maury, and Pierre Bontron. Filtering TOBIAS combinatorial test suites. In Proceedings of ETAPS/FASE'04 - Fundamental Approaches to Software Engineering, Barcelona, pages 281-294. Vol. 2984 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 2004. [PDF]
  The original publication is available at http://www.springerlink.com.
• Tao Xie, Darko Marinov, and David Notkin. Rostra: A Framework for Detecting Redundant Object-Oriented Unit Tests. In Proceedings of 19th Int. IEEE Conf. on Automated Sofware Engineering (ASE'04), Linz, pages 196-205. IEEE Computer Society Press, September, 2004. [PDF]
• Lydie du Bousquet, Yves Ledru, Olivier Maury, and Pierre Bontron. A case study in JML-based software validation. In Proceedings of 19th Int. IEEE Conf. on Automated Sofware Engineering (ASE'04), Linz, pages 294-297. IEEE Computer Society Press, September, 2004. [PDF]
• Bart Jacobs and Erik Poll. Java Program Verification at Nijmegen: Developments and Perspective. In Software Security - Theories and Systems: Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003, p. 134-153. Volume 3233 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 2004. [PDF] [Postscript] The original publication is available at http://www.springerlink.com.
• Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML. Journal of Logic and Algebraic Programming, 58(1-2):89-106, January-March 2004. [Original at sciencedirect.com] [Preprint postscript]
• Bart Jacobs. Weakest Precondition Reasoning for Java Programs with JML Annotations. Journal of Logic and Algebraic Programming, 58(1-2):61-88, January-March 2004. [Original at sciencedirect.com] [Preprint Postscript].
• Bart Jacobs. Martijn Oostdijk, and Martin Warnier. Source Code Verification of a Secure Payment Applet. Journal of Logic and Algebraic Programming, 58(1-2):107-120, January-March 2004. [Original at sciencedirect.com]
• Guoqing Xu and Zongyuan Yang. JMLAutoTest: A Novel Automated Testing Framework based on JML and JUnit. In 3rd IEEE ASE workshop on Formal Approaches to Testing of Software (FATES' 03), Monteal, Canada, October 2003. Volume 2931 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 2004, pages 118-127. [PDF] [Postscript] The original publication is available at http://www.springerlink.com.
• Joseph Kiniry and Erik Poll. Opportunities and challenges for formal specification of Java programs. In Trusted Components Workshop, Prato, Italy, January 2003. [PDF]
• L. Burdy, A. Requet, J.-L. Lanet. Java Applet Correctness: a Developer-Oriented Approach. In Stefania Gnesi, Keijiro Araki, and Dino Mandrioli (Eds.), FME 2003, International Symposium of Formal Methods Europe, Pisa, Italy, Sept. 8-14, 2003, Proceedings, pages 422-439. Volume 2805 of Lecture Notes in Computer Science, Springer Verlag, 2003. [Postscript].
• Néstor Cataño and Marieke Huisman. Chase: A Static checker for JML's Assignable Clause. In the proceedings of Verification, Model Checking and Abstract Interpretation (VMCAI '03), pages 26-40. Volume 2575 of Lecture Notes in Computer Science, Springer Verlag, 2003. [Postscript]
• Patrice Chalin. JML Support for Primitive Arbitrary Precision Numeric Types: Definition and Semantics, in Journal of Object Technology, 3(6):57-79, June 2004, http://www.jot.fm/issues/issue_2004_06/article3.
• Engelbert Hubbers and Erik Poll. Reasoning about Card Tears and Transactions in Java Card. In FASE'04 (Fundamental Approaches to Software Engineering), Barcelona, March 2004, pages 114-128. Volume 2984 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 2004. [PDF] [Postscript] The original publication is available at http://www.springerlink.com.
• Michael Peck. Improving the Usability of the ESC/Java Static Analysis Tool. Bachelor's Thesis, University of Virginia, March 2004. [PDF]
• Engelbert Hubbers, Martijn Oostdijk, and Erik Poll. Implementing a Formally Verifiable Security Protocol in Java Card. In Proceedings of SPC'2003, First International Conference on Security in Pervasive Computing, Boppard, Germany, pages 213-226. Volume 2802 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 2004. [PDF] The original publication is available at http://www.springerlink.com.
• Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael Ernst, Joseph Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An Overview of JML Tools and Applications. In International Journal on Software Tools for Technology Transfer, 7(3):212-232, June 2005. [PDF] The original publication is available at http://www.springerlink.com from http://dx.doi.org/10.1007/s10009-004-0167-4.
• Mike Barnett and David A. Naumann Wolfram Schulte and Qi Sun. 99.44\% pure: Useful Abstractions in Specification. In E. Poll (editor), ECOOP Workshop FTfJP'2004 Formal Techniques for Java-like Programs, Oslo, Norway, June 15, 2004. ICIS report NIII-R0426, pages 51-60, 2004. [PDF]
• David R. Cok. Reasoning with specifications containing method calls in JML and first-order provers. In E. Poll (editor), ECOOP Workshop FTfJP'2004 Formal Techniques for Java-like Programs, Oslo, Norway, June 15, 2004. ICIS report NIII-R0426, pages 41-48, 2004. [PDF]
• Yoonsik Cheon and Gary T. Leavens. The JML and JUnit Way of Unit Testing and its Implementation. Department of Computer Science, Iowa State University, TR #04-02a, February 2004, revised April 2004. [abstract] [postscript] [PDF]
• Bart Jacobs, Joseph Kiniry, and Martin Warnier. Java Program Verification Challenges. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (eds.), Formal Methods for Components and Objects, pages 202-219. Volume 2852 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 2003.
• Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok. How the Design of JML Accommodates Both Runtime Assertion Checking and Formal Verification. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (eds.), Formal Methods for Components and Objects, pages 262-284. Volume 2852 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 2003.
  Also Department of Computer Science, Iowa State University, TR #03-04, March 2003. [abstract] [PDF] [PostScript]
• Mehdi Kessis. Test de Conformité des programmes JAVA. Master's thesis, DEA Systèmes d'Information, Universite Joseph Fourier, 2003. [PDF] (in French).
• Robby, Edwin Rodríguez, Matthew B. Dwyer, and John Hatcliff. Checking Strong Specifications Using An Extensible Software Model Checking Framework, October 2003. Kansas State University, Department of Computer and Information Sciences, Technical Report, SAnToS-TR2003-10. [PDF]
• Daniel Larsson and Wojciech Mostowski. Specifying Java Card API in OCL. In Peter H. Schmitt (ed.), OCL 2.0 Workshop at UML 2003 Conference, San Francisco, USA, October 21, 2003, pages 3-19. Volume 102C of Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, 2004. [PDF]
• Cees-Bart Breunesse and Erik Poll. Verifying JML specifications with model fields. In Fifth ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP'2003), Darmstadt, Germany, pages 51-60. Technical Report 408, ETH Zurich, July 2003. [PDF]
• Engelbert Hubbers, Martijn Oostdijk, and Erik Poll. From Finite State Machines to Provably Correct JavaCard Applets. In Workshop of IFIP WG 11.2 - Small Systems Security, SEC'2003 (18th IFIP International Information Security Conference), Athens, May 2003. [PDF]
• Joe Verzulli. Getting started with JML: Improve your Java programs with JML annotation. IBM DeveloperWorks article, March 2003. [Web page at IBM DeveloperWorks] [PDF] [Chinese translation]
• Patrice Chalin. JML Support for Primitive Arbitrary Precision Numeric Types: Definition and Semantics. Technical Report CU-CS 2003-002.2a, Computer Science Department, Concordia University, June 2003. [PDF]
• Patrice Chalin. Improving JML: For a Safer and More Effective Language. In Stefania Gnesi, Keijiro Araki, and Dino Mandrioli (Eds.), FME 2003, International Symposium of Formal Methods Europe, Pisa, Italy, Sept. 8-14, 2003, Proceedings. Preliminary version available as Technical Report CU-CS 2003-001.2, Computer Science Department, Concordia University, March 2003, updated May 2003. [PDF]
• Yoonsik Cheon. A Runtime Assertion Checker for the Java Modeling Language. Department of Computer Science, Iowa State University, TR #03-09, April 2003. [abstract] [PDF] [PostScript]
• Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael Ernst, Joseph Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An Overview of JML Tools and Applications. In Thomas Arts and Wan Fokkink (editors), Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS '03), pages 73--89. Volume 80 of Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier, June, 2003. See also Department of Computer Science, University of Nijmegen, NIII-R0309, Nijmegen, March 2003. [PDF]
• Jianjun Zhao and Martin Rinard. Pipa: A Behavioral Interface Specification Language for AspectJ. Proc. Fundamental Approaches to Software Engineering (FASE'2003) of ETAPS'2003, Warsaw, Poland, April 5-13, 2003, pages 150-165. Volume 2621 of Lecture Notes in Computer Science, Springer Verlag. [PDF] [PostScript]
• Fausto Spoto and Erik Poll. Static Analysis for JML's assignable Clauses. In Proceedings of FOOL 10 (International Workshop on Foundations of Object-Oriented Languages), New Orleans, January 2003. [PDF] [Postscript]
• Lilian Burdy, Antonine Requet, J.-L. Lanet. JACK: Java Applet Correctness Kit. In 4th Gemplus Developer Conference, Singapore, November 2002. [PDF].
• K. Rustan M. Leino, Arnd Poetzsch-Heffter, and Yunhong Zhou. Using data groups to specify and check side effects. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 37(5) of SIGPLAN Notices, pages 246-257. ACM, May 2002. [PostScript]
• Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for Java. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 37(5) of SIGPLAN Notices, pages 234-245. ACM, May 2002. [PostScript] [PDF]
• Richard Paige, Liliya Kaminskaya, Jonathan Ostroff, and Jason Lancaric. BON-CASE: An Extensible CASE Tool for Formal Specification and Reasoning. in Journal of Object Technology, vol. 1 no. 3, Special issue: TOOLS USA 2002 proceedings, pages 77-96, http://www.jot.fm/issues/issue_2002_08/article5.
• Erik Poll, Pieter Hartel, and Eduard de Jong. A Java Reference Model of Transacted Memory for Smart Cards. In Proceedings of CARDIS'2002, Fifth Smart Card Research and Advanced Application Conference, pages 75-86. USENIX, 2002. [PDF]
• Ali Hamie Towards Verifying Java Realizations of OCL-Constrained Design Models Using JML. In 6th IASTED International Conference on Software Engineering and Applications, MIT, Cambridge, USA, 2002. [PDF]
• Patrice Chalin. Back to Basics: Language Support and Semantics of Basic Infinite Integer Types in JML and Larch Technical Report CU-CS 2002-003.2, Computer Science Department, Concordia University, October 2002. Updated March 2003. [PDF]
• Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Specification of Frame Properties in JML. Concurrency and Computation: Practice and Experience, 15(2):117-154, February, 2003. http://dx.doi.org/10.1002/cpe.713
  Also Department of Computer Science, Iowa State University, TR #02-02a, February 2002, revised October 2002. [abstract] [postscript] [PDF]
• Sarfraz Khurshid, Darko Marinov, and Daniel Jackson. An Analyzable Annotation Language. In 17th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2002), Seattle, WA. Nov 2002. (Available on-line from the MulSaw web page.)
• Chandrasekhar Boyapati, Sarfraz Khurshid, and Darko Marinov. Korat: Automated Testing Based on Java Predicates. In Proceedings International Symposium on Software Testing and Analysis (ISSTA), pages 123-133. ACM, July 2002. [PDF]
• Kerry Trentelman and Marieke Huisman Extending JML Specifications with Temporal Logic. In AMAST '02: Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, pages 334-348. Volume 2422 of Lecture Notes in Computer Science, Springer-Verlag, 2002. [Postscript]
• Néstor Cataño and Marieke Huisman Formal specification of Gemplus' electronic purse case study using ESC/Java. In proceedings of Formal Methods Europe (FME 2002), pages 272-289. Number 2391 of Lecture Notes in Computer Science, Springer Verlag, 2002.
  [Postscript] The corresponding ESC/Java annotations are also available.
• Yoonsik Cheon and Gary T. Leavens. A Runtime Assertion Checker for the Java Modeling Language (JML). In Hamid R. Arabnia and Youngsong Mun (eds.), International Conference on Software Engineering Research and Practice (SERP '02), Las Vegas, Nevada. CSREA Press, June 2002, pages 322-328.
  Also Department of Computer Science, Iowa State University, TR #02-05, March 2002. [abstract] [PDF]
• Yoonsik Cheon and Gary T. Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In Boris Magnusson (ed.), ECOOP 2002 -- Object-Oriented Programming, 16th European Conference, Malaga, Spain, June 2002, Proceedings. Volume 2374 of Lecture Notes in Computer Science, Springer Verlag, 2002, pages 231-255. The original publication is available at springerlink.com from http://www.springerlink.com/content/2yjt7jdnduntpgwp/.
  Also Department of Computer Science, Iowa State University, TR #01-12a, November 2001, revised March 2002. [abstract] [postscript] [PDF]
• Joachim van den Berg, Cees-Bart Breunesse Bart Jacobs, and Erik Poll. On the Role of Invariants in Reasoning about Object-Oriented Languages In Third ECOOP workshop on Formal Techniques for Java-like Programs (FTfJP'2001), Budapest, Hungary. [Abstract] [PDF]
• Krishna Kishore Dhara and Gary T. Leavens. Preventing Cross-Type Aliasing for More Practical Reasoning. Department of Computer Science, Iowa State University, TR #01-02a, March 2001, revised November 2001. [abstract] [postscript] [PDF]
• Erik Poll, Joachim van den Berg, and Bart Jacobs. Formal Specification of the JavaCard API in JML: the APDU class, Computer Networks, Volume 36, Issue 4, pages 407-421, Elsevier 2001. [PDF]
• Hung-Yu Lin. Executing Quantified Expressions in the JML Run-time Assertion Checker. Master's paper at The Pennsylvania State University, Capital College, August 2001. [PDF]
• Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Specification of Frame Properties in JML. In the Formal Techniques for Java Programs 2001, workshop at ECOOP 2001.
  Also Department of Computer Science, Iowa State University, TR #01-03, April 2001. [abstract] [postscript] [PDF]
• Marieke Huisman. Reasoning about {Java} Programs in higher order logic with PVS and Isabelle. Ph.D. dissertation, University of Nijmegen, Holland, February 2001. IPA Dissertation Series, 2001-03. [Postscript]
• Bart Jacobs, Hans Meijer and Erik Poll. VerifiCard: A European Project for Smart Card Verification. Newsletter 5 of the Dutch Association for Theoretical Computer Science (NVTI), 2001. [Postscript]
• Bart P. F. Jacobs and Erik Poll. A Logic for the Java Modeling Language JML. In Fundamental Approaches to Software Engineerin (FASE'2001), Genova, Italy. Volume 2029 of Lecture Notes in Computer Science, Springer Verlag, 2001, pages 284-299.
  An earlier version was Technical Report CSI-R0018, Computing Science Institute, University of Nijmegen, December, 2000.
• Clyde Ruby and Gary T. Leavens. Safely Creating Correct Subclasses without Seeing Superclass Code. In OOPSLA 2000 Conference Proceedings, pages 208-228. Volume 35, number 10 of ACM SIGPLAN Notices, October 2000. http://doi.acm.org/10.1145/353171.353186
  Also Department of Computer Science, Iowa State University, TR #00-05d, April 2000, revised April, June, July 2000. [abstract] [postscript] [PDF]
• Joachim van den Berg, Erik Poll, and Bart Jacobs. First steps in formalising JML. In S. Drossopoulou and S. Eisenbach and B. Jacobs and G. T. Leavens and P. Müller and A. Poetzsch-Heffter (eds.), Second ECOOP workshop on Formal Techniques for Java Programs (FTfJP'2000),, Sophia Antipolis, France, pages 103-110. [Postscript]
• Arun D. Raghavan. Design of a JML documentation generator. Department of Computer Science, Iowa State University, TR #00-12, March 2000. [abstract] [postscript]
• Abhay Bhorkar. A Run-time Assertion Checker for Java using JML. Department of Computer Science, Iowa State University, TR #00-08, May 2000. [abstract] [postscript].
• Erik Poll, Joachim van den Berg, and Bart Jacobs. Specification of the JavaCard API in JML. In J. Domingo-Ferrer, D. Chan, and A. Watson, editors, Smart Card Research and Advanced Application, pages 135-154. Kluwer Academic Publishers, 2000.
  Also Department of Computer Science, University of Nijmegen. CSI report CSI-R0005, February, 2000.
• Gary T. Leavens and Albert L. Baker. Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. In Jeannette M. Wing, James Woodcock, and Jim Davies (editors). FM'99 -- Formal Methods: World Congress on Formal Methods in Development of Computer Systems, Toulouse, France, September 1999, pages 1087--1106. Volume 1709 of Lecture Notes in Computer Science, Springer Verlag, 1999.
  Also: Department of Computer Science, Iowa State University, TR #97-19b, September 1997, revised February, June 1999.

See also the researchers named for less directly related publications.

Last modified Wednesday, August 1, 2007.