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. Please send a citation for your paper (in XHTML, please, with links for each author and a link to a PDF file) to Gary Leavens (leavens@ucf.edu).

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 (leavens@eecs.ucf.edu).

• Ijaz Ahmed and Nestor Catano. Checking JML-Encoded Finite State Machine Properties. In 2018 International Conference on Advancements in Computational Sciences (ICACS), Lahore, Pakistan, pages 1-9. https://doi.org/10.1109/ICACS.2018.8333496
• Peter W. V. Tran-Jorgensen, Peter Gorm Larsen, and Gary T. Leavens. Automated translation of VDM to JML-annotated Java. International Journal on Software Tools for Technology Transfer. 20(2):211-235, 2018. Available from http://rdcu.be/GIi1 and http://dx.doi.org/10.1007/s10009-017-0448-3
• Wenhui Sun, Yuting Sun, Zhifei Zhang, Jingpeng Tang, Kendall E. Nygard, and Damian Lampl. Specification and Verification of Garbage Collector by Java Modeling Language. In FUTURE COMPUTING 2015 : The Seventh International Conference on Future Computational Technologies and Applications, March 2015, Nice France, pages 18-23. https://www.researchgate.net/publication/289317248
• Stijn de Gouw, Jurriaan Rot, Frank S. de Boer, Richard Bubel, and Reiner Häahnle. OpenJDK's java.utils.Collection.sort() is broken: The good, the bad, and the worst case. To appear in CAV'15. There is a blog post about it, which links to a [Preprint PDF].
• Enforcing information hiding in interface specifications: a client-aware checking approach

  Henrique Rebêlo, Gary T. Leavens
  MODULARITY Companion 2015 Companion Proceedings of the 14th International Conference on Modularity, 2015
• AspectJML: modular specification and runtime checking for crosscutting contracts

  Henrique Rebêlo, Gary T. Leavens, Mehdi Bagherzadeh, Hridesh Rajan, Ricardo Lima, Daniel M. Zimmerman, Márcio Cornélio, Thomas Thüm
  MODULARITY '14 Proceedings of the 13th international conference on Modularity, 2014
• Modularizing crosscutting contracts with AspectJML

  Henrique Rebêlo, Gary T. Leavens, Mehdi Bagherzadeh, Hridesh Rajan, Ricardo Lima, Daniel M. Zimmerman, Márcio Cornélio, Thomas Thüm
  MODULARITY '14 Proceedings of the companion publication of the 13th international conference on Modularity, 2014
• Alysson Milanez, Dennis Sousa, Tiago Massoni, and Rohit Gheyi. JMLOK2: A tool for detecting and categorizing nonconformances. In CBSoft2014: Congresso Braaileiro de Software: Teoria e Pratica, Sept 28 to October 3, 2014, pages 69-76. http://www.ic.ufal.br/evento/cbsoft2014/anais/ferramentas_v1_p.pdf
• Waldimir Araujo, Lionel C. Briand, Yvan Labiche. On the Effectiveness of Contracts as Test Oracles in the Detection and Diagnosis of Functional Faults in Concurrent Object-Oriented Software. IEEE Transactions on Software Engineering, 40(10):971-992, October 2014. http://dx.doi.org/10.1109/TSE.2014.2339829
• Néstor Cataño and Víctor Rivera. "Translating Event-B to JML-specified Java Programs" In Proceedings of 29th ACM Symposium on Applied Computing, Software Verification and Testing track (SAC-SVT). [PDF]
• Static verification of ptolemyrely programs using openJML

  José Sánchez, Gary T. Leavens
  FOAL '14 Proceedings of the 13th workshop on Foundations of aspect-oriented languages, 2014
• Client-aware checking and information hiding in interface specifications with JML/ajmlc

  Henrique Rebêlo, Gary T. Leavens, Ricardo Massa Lima
  SPLASH '13 Proceedings of the 2013 companion publication for conference on Systems, programming, & applications: software for humanity, 2013
• Wladimir Araujo, Lionel C. Briand, and Yvan LaBiche. On the Effectiveness of Contracts as Test Oracles in the Detection and Diagnosis of Faults in Concurrent Object-Oriented Software. Carleton University Technical Report SCE-13-04, September 2013. [TR PDF].
• Henrique Rebêlo, Gary T. Leavens, Mehdi Bagherzadeh, Hridesh Rajan, Ricardo Lima, Daniel M. Zimmerman, Márcio Cornélio, and Thomas Thüm. AspectJML: Modular Specification and Runtime Checking for Crosscutting Contracts. To appear in Modularity 2014.
  [abstract] [Preprint PDF]
• Henrique Rebêlo, Ricardo Lima, Gary T. Leavens, Márcio Cornélio, Alexandre Mota, and César Oliveria. Optimizing Generated Aspect-Oriented Assertion Checking Code for JML Using Program Transformations: An Empirical Study. Science of Computer Programming, 78(8):1137-1156, Aug. 2013. http://dx.doi.org/10.1016/j.scico.2012.09.003
• Gary T. Leavens, Peter H. Schmitt, and Jooyong Yi. The Java Modeling Language. NII Shonan Meeting Report, Number 2013-3, May 2013. http://www.nii.ac.jp/shonan/wp-content/uploads/2011/09/No.2013-3.pdf.
• Juan P. Galeotti, Nicolás Rosner, Carlos G. López Pombo, and Marcelo F. Frias. TACO: Efficent SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds. IEEE Transactions on Software Engineering 39(9):1283-1307, Sep. 2013. http://dx.doi.org/10.1109/TSE.2013.15
• Modular aspect-oriented design rule enforcement with XPIDRs

  Henrique Rebelo, Gary T. Leavens, Ricardo Massa Ferreira Lima, Paulo Borba, Márcio Ribeiro
  FOAL '13 Proceedings of the 12th workshop on Foundations of aspect-oriented languages, 2013, pp. 13-18.
• Néstor Cataño, Tim Wahls, Camilo Rueda, Víctor Rivera, and Danni Yu. Translating B Machines to JML Specifications. In Proceedings of the 27th Annual ACM Symposium on Applied Computing (SAC '12), pages 1271-1277, ACM, 2012. http://dx.doi.org/10.1145/2245276.2231978 Preprint at [Preprint PDF].
• Henrique Rebêlo, Ricardo Lima, Alexandre Mota, César Oliveria, and Márcio Ribeiro. Enforcing Contracts for Aspect-Oriented Programs with Annotations, Pointcuts and Advice. In Proceedings of the 24rd International Conference on Software Engineering and Knowledge Engineering (SEKE 2012), San Francisco Bay, USA, July 1-3, 2012, pages 148-153. The original publication is available at SEKE2012 Proceedings. Also won the best demo Award.
• Shin Hwei Tan, Darko Marinov, Lin Tan and Gary T. Leavens. @tComment: Testing Javadoc Comments to Detect Comment-Code Inconsistencies. In Fifth International Conference on Software Testing, Verification and Validation (ICST 2012), Montreal, April 2012, pages 260-269. The original publication is at http://doi.ieeecomputersociety.org/10.1109/ICST.2012.106.
• Henrique Rebêlo, Ricardo Lima, and Márcio Cornélio. Implementing JML Contracts with AspectJ: Improving instrumentation and checking of JML contracts. Book published by LAP Lambert Academic Publishing, Germany, 2012. (ISBN: 384733753X, 9783847337539)
• Joseph R. Kiniry, Daniel M. Zimmerman, and Ralph Hyland. "Testing Library Specifications by Verifying Conformance Tests". In 6th International Conference on Tests & Proofs (TAP '12), Prague, Czech Republic, May 2012. Volume 7305 of Lecture Notes in Computer Science, Springer-Verlag, 2012.
  The original publication is available at springerlink.com at http://dx.doi.org/10.1007/978-3-642-30473-6_6.
  Also [Preprint PDF]
• Henrique Rebêlo, Gary T. Leavens, and Ricardo Lima. Modular Enforcement of Supertype Abstraction and Information Hiding with Client-Side Checking. Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-12-03, January 2012. [abstract] [Preprint PDF]
• Néstor Cataño, Camilo Rueda, and Sorren Hanvey. Verification of JML Generic Types with Yices. In Proceedings of 6th Colombian Congress of Computing (6CCC), 2011. [PDF]
• Hermann Lehner. A Formal Definition of JML in Coq and its Application to Runtime Assertion Checking. Ph.D. Thesis, ETH Zurich, 2011. [PDF] Coq sources available at jmlcoq.info/.
• Néstor Cataño, João Pestana, and Ricardo Rodrigues. JFly: A JML-Based Strategy for Incorporating Formal Specifications into the Software Development Process. In INFORUM 2010. [PDF]
• Hermann Lehner and Peter Müller. Efficient Runtime Assertion Checking of Assignable Clauses with Datagroups In Fundamental Approaches to Sofware Engineering (FASE) 2010, pages 338-352. Volume 6013 of Lecture Notes in Computer Science, Springer-Verlag, 2010.
  The original publication is available at springerlink.com at http://www.springerlink.com/content/1jqj3086l8734p37/.
• Henrique Rebêlo, Gary T. Leavens, and Ricardo Lima. Modular Enforcement of Supertype Abstraction and Information Hiding with Client-Side Checking. Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-11-07a, October 2011, revised December 2011. [abstract] [Preprint PDF]
• Henrique Rebêlo. Towards Client-Aware Interface Specifications. In Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion (SPLASH '11), Portland, Oregon, USA, October 22-27, 2011. To appear. [PDF].
• Henrique Rebêlo, Ricardo Lima, and Gary T. Leavens. Modular Contracts with Procedures, Annotations, Pointcuts and Advice. To appear in the proceedings of the XV Brazilian Symposium on Programming Languages (SBLP 2011), Sao-Paulo, Brazil, September 29-30, 2011.
  Also Technical report CS-TR-11-05, Dept. of Electrical Engineering and Computer Science, University of Central Florida, September 2011. [abstract] [PDF]
• Henrique Rebêlo, Ricardo Lima, Uirá Kulesza, Cláudio Sant'Anna, Roberta Coelho, Alexandre Mota, Márcio Ribeiro, and César Oliveria. Assessing the Impact of Aspects on Design By Contract Effort: A Quantitative Study. In Proceedings of the 23rd International Conference on Software Engineering and Knowledge Engineering (SEKE 2011), Miami, USA, July 7-9, 2011, pages 450-455. The original publication is available at SEKE2011 Proceedings.
• Ghaith Haddad and Gary T. Leavens. Specifying Subtypes in SCJ Programs. Concurrency and Computation Practice and Experience, 25(16):2290-2306, November 2013, John Wiley & Sons, Ltd. Online October 4, 2012 at http://dx.doi.org/10.1002/cpe.2930.
• Wladimir Araujo, Lionel C. Briand, and Yvan LaBiche. Enabling the Runtime Assertion Checking of Concurrent Contracts for the Java Modeling Language. In ICSE 2011 Proceedings, Waikiki, Honolulu, HI, USA, pages 786-795.
• David Cok. OpenJML: JML for Java 7 by Extending OpenJDK. In Mihaela Bobaru, Klaus Havelund, Gerard Holzmann, and Rajeev Joshi (eds.), NASA Formal Methods, pages 472-479. Volume 6617 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 2011. The original publication is available from springerlink.com at http://dx.doi.org/10.1007/978-3-642-20398-5_35.
• Daniel Bruns. Eine formale Semantik für die Java Modeling Language. (German version of the workshop paper below.) To appear in Informatik-Spektrum, Springer-Verlag, 2011. [PDF]
• Henrique Rebêlo, Roberta Coelho, Ricardo Lima, Gary T. Leavens, Marieke Huisman, Alexandre Mota, and Fernando Castor. On the Interplay of Exception Handling and Design by Contract: An Aspect-Oriented Recovery Approach. In FTFJP'11: Proceedings of the 13th Workshop on Formal Techniues for Java-Like Programs, article 7, 2011. http://dx.doi.org/10.1145/2076674.2076681
  Also Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-11-02, April 2011. [Abstract] [Preprint PDF]
• José Elias Araújo, Henrique Rebêlo, Ricardo Lima, Alexandre Mota, Uirá Kulesza, and Cláudio Sant'Anna. An Annotation-Based Approach for JCSP Concurrent Programming: A Quantitative Study. In Proceedings of the 1st workshop on Modularity in systems software (MISS 2011), Porto de Galinhas , Pernambuco, Brazil, March 22, 2011, pages 7-11. http://dx.doi.org/10.1145/1960518.1960521 [PDF]
• Benjamin Weiß, Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. Ph.D. thesis, Karlsruhe Institute of Technology, Karlsruhe, Germany. KIT Scientific Publishing, 2011. [PDF]
• Daniel Bruns, Vladimir Klebanov, and Ina Schaefer. Verification of Software Product Lines with Delta-oriented Slicing. In International Conference on Formel Verification of Object-oriented Software (FoVeOOS 2010), revised selected papers, Lecture Notes in Computer Science, Vol. 6528, Springer-Verlag, 2011. [PDF]
• Henrique Rebêlo, Ricardo Lima, Uirá Kulesza, Roberta Coelho, Alexandre Mota, Márcio Ribeiro and José Elias Araújo. The Contract Enforcement Aspect Pattern. In SugarLoafPLop 2010: Proceedings of the 8th Latin American Conference on Pattern Languages of Programming , Salvador, Brazil, September 2010. [PDF]
• Faraz Hussain and Gary T. Leavens. temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties. In SEFM 2010: Proceedings of the 8th International Conference on Software Engineering and Formal Methods, Pisa, Italy, September 2010, pages 63-72, IEEE.
  Also Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-10-08, July 2010. [Preprint PDF]
• Ghaith Haddad, Faraz Hussain, and Gary T. Leavens. The Design of SafeJML, a Specification Language for SCJ with Support for WCET Specification. In JTRES '10: Proceedings of the 8th International Workshop on Java Technologies for Real-Time and Embedded Systems, Prague, August 2010, pages 155-163. [PDF]
  Also Dept. of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-10-06, June 2010. [Preprint PDF]
• Perry Roland James. Enhancements to JML and its Extended Static Checking Technology. Ph.D. thesis, Concordia University, Montreal, Quebec, Canada, July 2009. [PDF]
• Piotr Kosiuczenko. On the Implementation of @pre. In Fundamental Approaches to Sofware Engineering (FASE) 2009, pages 246 - 261. Volume 5503 of Lecture Notes in Computer Science, Springer-Verlag, 2009.
  The original publication is available at springerlink.com
  [Preprint PDF]
• Juan P. Galeotti, Nicolás Rosner, Carlos G. López Pombo, and Marcelo F. Frias. Analysis of Invariants for Efficient Bounded Verification. To appear in ISSTA '10. [Prepreint PDF]
• Bernhard Beckert, Daniel Bruns, and Sarah Grebing. Mind the Gap: Formal Verification and the Common Criteria. In 6th International Verification Workshop (VERIFY-2010), Edinburgh, UK, 2010. [Preprint PDF]
• Daniel Bruns. Formal Semantics for the Java Modeling Language Extended abstract. In Informatiktage 2010, Bonn, Germany. To appear in Lecture Notes in Informatics, Vol. S-9. [Preprint PDF]
• Amritam Sarcar and Yoonsik Cheon. A New Eclipse-Based JML Compiler Built Using AST Merging. Technical Report 10-08, Department of Computer Science, University of Texas at El Paso, El Paso, TX, March 2010. [PDF]
• Ádám Peter Darvas. Reasoning About Data Abstraction in Contract Languages. Ph.D. dissertation, ETH Zurich, Diss ETH No. 18622, 2009. [PDF]
• Werner Dietl. Universe Types: Topology, Encapsulation, Genericity, and Tools. Ph.D. dissertation, ETH Zurich, Diss ETH No. 18522, 2009. [Abstract + PDF]
• Taekgoo Kim, Kevin Bierhoff, Jonathan Aldrich, and Sungwon Kang. Typestate Protocol Specification in JML. In Specification and Verification of Component-Based Systems (SAVCBS'09), 2009. To appear.
• Perry R. James and Patrice Chalin. ESC4: A Modern Caching ESC for Java. In Specification and Verification of Component-Based Systems (SAVCBS'09), 2009. To appear.
• Marieke Huisman. On the Interplay between the Semantics of Java's Finally Clauses and the JML Run-Time Checker. In Formal Techniques for Java-Like Programs 2009 (FTfJP), July, 2009.
  [Preprint PDF]
• Daniel Bruns. Formal Semantics for the Java Modeling Language. Diploma thesis, Institute for Theoretical Computer Science, University of Karlsruhe, Germany, June 2009. [PDF]
• Marieke Huisman and Alejandro Tamalet. A Formal Connection between Security Automata and JML Annotations. In Fundamental Approaches to Sofware Engineering (FASE) 2009, pages 340-354. Volume 5503 of Lecture Notes in Computer Science, Springer-Verlag, 2009.
  The original publication is available at springerlink.com
  [Preprint PDF]
• Henrique Rebêlo, Ricardo Lima, Márcio Cornélio, Gary T. Leavens, Alexandre Mota, and César Oliveira. Optimizing JML Feature Compilation in Ajmlc Using Aspect-Oriented Refactorings. In the proceedings of the XIII Brazilian Symposium on Programming Languages (SBLP 2009), Gramado-RS, Brazil, August 19-21, 2009.
  Also Technical report CS-TR-09-05, School of Electrical Engineering and Computer Science, University of Central Florida, April 2009. [abstract] [PDF]
• Faraz Hussain. Enhancing a behavioral interface specification language with temporal logic features. Department of Computer Science, Iowa State University, TR #09-18, April 2009. [abstract] [PDF]
• Perry R. James and Patrice Chalin, Extended Static Checking in JML4: Benefits of Multiple-Prover Support. In Proceedings of the ACM Symposium on Applied Computing, Software Verification and Testing Track (SAC-SVT), Hawaii, March, 2009. [PDF]
• Nestor Catano and Tim Wahls, Executing JML Specifications of Java Card Applications: A Case Study. In Proceedings of the ACM Symposium on Applied Computing, Software Engineering Track (SAC-SE), Hawaii, March, 2009. pages 404 - 408. [PDF]
• Robby and Patrice Chalin. Preliminary Design of a Unified JML Representation and Software Infrastructure. Technical Report SAnToS-TR2009-04-01, SAnToS Laboratory, Department of Computing and Information Sciences, Kansas State University, April, 2009. [PDF]
• John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, and Matthew Parkinson. Behavioral Interface Specification Languages. School of EECS, University of Central Florida, CS-TR-09-01, March 2009. [abstract] [PDF]
• Steve M. Shaner. Modular verification of higher-order methods with mandatory calls specified by model programs. Department of Computer Science, Iowa State University, TR #09-16, January 2009. [abstract] [PDF]
• Néstor Cataño, Fernando Barraza, Daniel García, Pablo Ortega, and Camilo Rueda. A Case Study in JML-Assisted Software Development. In Brazilian Symposium on Formal Methods (SBMF), 2008. [PDF]
• Alain Giorgetti, , Julien Groslambert, Jacques Julliand, and Olga Kouchnarenko. Verification of class liveness properties with Java Modeling Language. IET Software, 2(6):500-514, IET, Dec. 2008.
  The original publication is available from http://dx.doi.org/10.1049/iet-sen:20080008.
• Jacek Chrzaszcz, Marieke Huisman, Aleksy Schubert, Joseph Kiniry, Mariela Pavlova, and Erik Poll. BML Reference Manual, 2008. In progress. See http://www.jmlspecs.org/BML
• Jacek Chrzaszcz, Marieke Huisman, and Aleksy Schubert. BML and related tools. In Software Technologies Concertation on Formal Methods for Components and Objects (FMCO 2008). Springer-Verlag, LNCS, To appear. [Preprint PDF]
• Wladimir Araujo, Lionel Briand, and Yvan Labiche. Concurrent Contracts for Java in JML. 19th International Symposium on Software Reliability Engineering (ISSRE), pages 37-46, November 2008.
• Perry R. James, Patrice Chalin, Leveda Giannas, and George Karabotsos. Distributed Multi-threaded Verification of Java Programs. Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008), pages 3-10, November 2008. [PDF]
• Henrique Rebêlo, Sergio Soares, Ricardo Lima, Paulo Borba, and Márcio Cornélio. JML and Aspects: The Benefits of Instrumenting JML Features with AspectJ . Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008), pages 11-18, November 2008. [PDF]
• George Karabotsos, Patrice Chalin, Perry R. James, and Leveda Giannas. Total Correctness of Recursive Functions using JML4 FSPV . Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008), pages 19-26, November 2008. [PDF]
• David R. Cok. Adapting JML to generic types and Java 1.6. Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008), pages 27-34, November 2008. [PDF]
• David R. Cok, and Gary T. Leavens. Extensions of the theory of observational purity and a practical design for JML. Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008), pages 43-50, November 2008. [PDF]
• Steve Shaner, Hridesh Rajan, and Gary T. Leavens. Model Programs for Preserving Composite Invariants. Seventh International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2008), pages 95-100, November 2008. [PDF]
• Umberto Costa, Anamaria Moreira, Martin Musicante, and Placido Souza Neto. Specification and Runtime Verification of Java Card Programs. In Brazilian Symposium on Formal Methods, SBMF'2008, Salvador, Brazil, 26th-29th October 2008. [Preprint PDF] [Preprint PS]
• Patrice Chalin, Perry R. James, and George Karabotsos. JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML. Technical report DSRG 2008-01x, 2008. [PDF]
• Henrique Rebêlo. Implementing JML Contracts with AspectJ. Master's thesis, Departamento de Sistemas e Computação, Universidade de Pernambuco, Recife, Brazil, May 2008. [PDF]
• Henrique Rebêlo, Ricardo Lima, Márcio Cornélio, and Sérgio Soares. A JML compiler based on AspectJ. In Proceedings of the 1st Internacional Conference on Software Testing, Verification, and Validation (ICST 2008), Lillehammer, Norway, April 9-11, 2008, pages 541-544. http://doi.ieeecomputersociety.org/10.1109/ICST.2008.14
• Kristina B. Taylor, Johannes Rieken, and Gary T. Leavens. Adapting the Java Modeling Language for Java 5 Annotations. Department of Computer Science, Iowa State University, TR #08-06, April 2008. [abstract] [PDF]
• Ghaith Haddad and Gary T. Leavens. Extensible Dynamic Analysis for JML: A Case Study with Loop Annotations. School of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-08-05, April 2008. [Preprint PDF]
• Kristina B. Taylor. A Specification Language Design for the Java Modeling Language (JML) Using Java 5 Annotations. Department of Computer Science, Iowa State University, TR #08-03, April 2008. [abstract] [PDF]
• Michael Moeller, Ernst-Ruediger Olderog, Holger Rasch, and Heike Wehrheim. Integrating a formal method into a software engineering process with UML and Java. Formal Aspects of Computing, 20(2):161-204, March 2008. The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/s00165-007-0042-7.
• Yoonsik Cheon, Antonio Cortes, Martine Ceberio, and Gary T. Leavens. Integrating Random Testing with Constraints for Improved Efficiency and Diversity. To appear in SEKE'08.
  Also University of Texas at El Paso, TR #08-07, February 2008. [Preprint PDF]
• Henrique Rebêlo, Ricardo Lima, Márcio Cornélio, Sérgio Soares, and Leopoldo Ferreira. Implementing Java Modeling Language Contracts with AspectJ. In Proceedings of the 23rd ACM Symposium on Applied Computing (SAC 2008), Programming Languages Track, Fortaleza , Ceará, Brazil, March 16-20, 2008, pages 228-233. http://doi.acm.org/10.1145/1363686.1363745 [Preprint PDF]
• Kristina P. Boysen and Gary T. Leavens. Discussion of Design Alternatives for JML Java 5 Annotations. Department of Computer Science, Iowa State University, TR #08-01, January 2008. [abstract] [PDF]
• Mark Royer, Suad Alagic, and Dan Dillon. Reflective Constraint Management for Languages on Virtual Platforms. Journal of Object Technoloby, 6(10):59-79, November-December 2007, http://www.jot.fm/issues/issue_2007_11/article1/. [PDF]
• Mikolás Janota, Radu Grigore, and Michal Moskal. Reachability Analysis for Annotated Code. Sixth International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2007), pages 23-30, September 2007. [PDF]
• Ádám Darvas and Peter Müller. Faithful mapping of model classes to mathematical structures. Sixth International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2007), pages 31-38, September 2007. [PDF]
• Patrice Chalin, Perry R. James, and George Karabotsos. An Integrated Verification Environment for JML: Architecture and Early Results. Sixth International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2007), pages 47-53, September 2007. [PDF]
• 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. In Formal Methods for Components and Objects (FMCO 2006), pages 152-174, volume 4709 of Lecture Notes in Computer Science, Springer-Verlag, 2007. The original publication is available at springerlink.com
  [Preprint PDF]
• 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]
• Modular verification of higher-order methods with mandatory calls specified by model programs

  Steve M. Shaner, Gary T. Leavens, David A. Naumann
  In International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), Montreal, Canada, October 2007, pages 351-367.
• Tao Xie, Kunal Tanja, 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. In Fundamental Approaches to Software Engineering (FASE 2007), pages 215-229, volume 4422 of Lecture Notes in Computer Science, Springer-Verlag, 2007. The original publication is available at springerlink.com
  [Preprint PDF]
• Julien Groslambert. JAG Extension for Verifying LTL Properties on B Event Systems. In B 2007: Formal Specification and Development in B, Besancon, France, pages 262-265. Volume 4355 of Lecture Notes in Computer Science, Springer-Verlag, January, 2007.
  The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/11955757_25.
• 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]
• Jacek Chrząszcz and Aleksy Schubert. ESC/Java2 as a Tool to Ensure Security in the Source Code of Java Applications In Krzysztof Sacha (ed), Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM), Warsaw, Poland, pages 337-348. Volume 227/2006 of IFIP International Federation for Information Processing, Springer-Verlag, 2006. [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, May, 2006.
  http://dx.doi.org/10.1145/1127878.1127884
  Also Department of Computer Science, Iowa State University, TR #98-06-rev29, January 2006. [abstract] [postscript] [PDF]
• Alain Giorgetti and Julien Groslambert. JAG: JML Annotation Generation for Verifying Temporal Properties. In Fundamental Approaches to Software Engineering, Vienna, Austria, pages 373-376. Volume 3922 of Lecture Notes in Computer Science, Springer-Verlag, March, 2006.
  The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/11693017_27.
• 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 is available at springerlink.com or directly from http://dx.doi.org/10.1007/11752707_9.
• 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. In Bertrand Meyer and Jim Woodcock (eds.), Verified Software: Theories, Tools, Experiments, Zürich, Switzerland, October, 2005, pages 134-143. Volume 4171 of Lecture Notes in Computer Science, Springer Verlag, 2008. The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/978-3-540-69149-5_15.
  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.
  
• 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]
• A contextual interpretation of undefinedness for runtime assertion checking

  Yoonsik Cheon, Gary T. Leavens
  AADEBUG'05 Proceedings of the sixth international symposium on Automated analysis-driven debugging, 2005, pp. 149-158.
• 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].
• Francoise Bellegarde, Julien Groslambert, Marieke Huisman, Olga Kouchnarenko, and Jacques Julliand. Verification of Liveness Properties with JML. INRIA Technical Report, nr. RR-5331, 2004. [Postscript]
• Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis 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]
• 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. 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.
• 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. [original at link.springer.com]
• 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. [Workshop proceedings 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 using 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]
• JML (poster session): notations and tools supporting detailed design in Java

  Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, Bart Jacobs
  OOPSLA '00 Addendum to the 2000 proceedings of the conference on Object-oriented programming, systems, languages, and applications (Addendum), 2000, pp. 105-106.
• 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 Friday, December 10, 2021.