The JML4 project has been superceded by JmlEclipse.
JML4, is the DSRG's proposal for an Integrated development and Verification Environment (IVE) for JML that builds upon Eclipse’s support for Java, enhancing it with
- Runtime Assertion Checking (RAC),
- Extended Static Checking (ESC) and
- Full Static Program Verification (FSPV).
Though it currently only supports a subset of JML, we believe that JML4 is the first IVE to support such a full range of verification techniques for a mainstream programming language. For details, see:
- 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, October 6-9, 2008.
- P. Chalin, P. R. James, and G. 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.
and
- 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.
- 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), November, 2008.
- 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), November, 2008.
