JmlEclipse is an Eclipse-based Integrated Verification Environment (IVE) for Java 5+ that offers its services via a deep integration with the Eclipse JDT. It uses the Java Modeling Language (JML) as a specification notation and it currently supports:

• Runtime Assertion Checking (RAC).
• Static Verification via Symbolic Execution.
• Test case generation, including the graphical representation of complex heap structures.

The former is achieved by JML4c, the JML4-based RAC tool by Amritam Sarcar and Yoonsik Cheon. The latter two features are offered by Sireum/Kiasan for Java by Robby and other members of the SAnToS team at Kansas State University (KSU).

JmlEclipse development is being lead by Patrice Chalin (DSRG.org) and Robby (SAnToS). For those of you how know a bit about the history of JML tools, JmlEclipse is the successor of JML4 (well, actually, successor of the various JMLn projects). It runs under Eclipse 3.5.2, reads JML specifications in the JML2 input syntax and emits classes files with JML embedded in the JML Intermediate Representation (JIR) format. For those of you who recall, this is actually a rebirth of the old SAnToS JmlEclipse plug-in.

JmlEclipse tooling papers:

• P. Chalin, Robby, P.R. James, J. Lee, G. Karabotsos, “Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML”, Int. J. on Software Tools for Technology Transfer (STTT), 12(6): 429-446, 2010. Preprint as Kansas State University, SAnToS-TR2009-10-01. Last updated: January, 2010.
• Robby and P. Chalin, “Preliminary Design of a Unified JML Representation and Software Infrastructure”. Proceedings of the 11th Workshop on Formal Techniques for Java-like Programs (FTfJP'09), Genova, Italy, July, 2009. (Extended TR version)

Other related papers include:

• P. Chalin, “Engineering a Sound Assertion Semantics for the Verifying Compiler”, IEEE Transactions on Software Engineering, 36(2):275-287, 2010. DOI; appendix.
• P. R. James and P. Chalin, “Faster and More Complete Extended Static Checking for the Java Modeling Language”, J. Automated Reasoning, 44(1-2):145-174, 2010. (SpringerLink)
• P. Chalin, P. R. James, and F. Rioux, “Reducing the Use of Nullable Types through Non-null by Default and Monotonic Non-null”, IET Software Journal, 2(6):515-531, 2008. DOI.

Previous papers on JML4:

• P. R. James and P. Chalin, “Extended Static Checking in JML4: Benefits of Multiple-Prover Support”. Proceedings of the ACM Symposium on Applied Computing, Software Verification and Testing Track (SAC-SVT), Hawaii, March 2009. [26%]
• P. R. James, P. Chalin, L. Giannas, and G. Karabotsos, “Distributed, Multi-threaded Verification of Java Programs”. Proceedings of the International Workshop on Specification and Verification of Component-Based Systems (SAVCBS), Atlanta, Georgia (USA), Nov. 2008. [40%]
• G. Karabotsos, P. Chalin, P. R. James, and L. Giannas, “Total Correctness of Recursive Functions using JML4 FSPV”. Proceedings of the International Workshop on Specification and Verification of Component-Based Systems (SAVCBS), Atlanta, Georgia (USA), Nov. 2008. [40%]
• P. Chalin, P. R. James, and G. Karabotsos, “JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML”. Proceedings of the International Conference on Verified Software: Theories, Tools, Experiments (VSTTE), Toronto, Canada, Oct. 6-9, 2008.