JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML

  • Patrice Chalin
  • Perry R. James
  • George Karabotsos
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)


Tool support for the Java Modeling Language (JML) is a very pressing problem. A main issue with current tools is their architecture: the cost of keeping up with the evolution of Java is prohibitively high: e.g., Java 5 has yet to be fully supported. This paper presents JML4, our proposal for an Integrated Verification Environment (IVE) for JML that builds upon Eclipse’s support for Java, enhancing it with Run time 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.


Proof Obligation Java Modeling Language Verification Technique Abstract Syntax Tree Risk Item 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY Tool. SoSyM 4, 32–54 (2005)CrossRefGoogle Scholar
  2. 2.
    Aspinall, D.: Proof General (2008),
  3. 3.
    Barnes, J.: High Integrity Software: The Spark Approach to Safety and Security. AW (2003)Google Scholar
  4. 4.
    Barnett, M., Leino, K.R.M.: Weakest-Precondition of Unstructured Programs. In: Workshop on Program Analysis for Software Tools and Engineering (PASTE), Lisbon, Portugal. ACM Press, New York (2005)Google Scholar
  5. 5.
    Barthe, G., Burdy, L., Charles, J., Grégoire, B., Huisman, M., Lanet, J.-L., Pavlova, M., Requet, A.: JACK: a tool for validation of security and behaviour of Java applications. In: Proceedings of the 5th International Symposium on Formal Methods for Components and Objects (FMCO) (2007)Google Scholar
  6. 6.
    Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An Overview of JML Tools and Applications. International Journal on Software Tools for Technology Transfer (STTT) 7(3), 212–232 (2005)CrossRefGoogle Scholar
  7. 7.
    Burdy, L., Huisman, M., Pavlova, M.: Preliminary Design of BML: A Behavioral Interface Specification Language For Java Bytecode. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol. 4422, pp. 215–229. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Burdy, L., Requet, A., Lanet, J.-L.: Java Applet Correctness: A Developer-Oriented Approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)Google Scholar
  9. 9.
    Chalin, P., James, P.R.: Non-null References by Default in Java: Alleviating the Nullity Annotation Burden. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  10. 10.
    Chalin, P., James, P.R., Karabotsos, G.: An Integrated Verification Environment for JML: Architecture and Early Results. In: Proceedings of the Sixth International Workshop on Specification and Verification of Component-Based Systems (SAVCBS), Cavtat, Croatia, September 3-4, pp. 47–53. ACM, New York (2007)Google Scholar
  11. 11.
    Chalin, P., James, P.R., Rioux, F., Karabotsos, G.: Towards a Verified Software Repository Candidate: Cross-Verifying a Verifier, Concordia University, Dependable Software Research Group Technical Report (2008)Google Scholar
  12. 12.
    Chalin, P., Kiniry, J., Leavens, G.T., Poll, E.: Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Cheon, Y.: A Runtime Assertion Checker for the Java Modeling Language, Iowa State University, Ph.D. Thesis, also TR #03-09 (April 2003)Google Scholar
  14. 14.
  15. 15.
    Cok, D.R., Kiniry, J.R.: ESC/Java2: Uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)Google Scholar
  16. 16.
    Deng, X., Robby, Hatcliff, J.: Kiasan/KUnit: Automatic Test Case Generation and Analysis Feedback for Open Object-oriented Systems, Kansas State University (2007)Google Scholar
  17. 17.
    Ernst, M., Coward, D.: Annotations on Java Types,, JSR 308, October 17 (2006)Google Scholar
  18. 18.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proc. of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), vol. 37(5), pp. 234–245. ACM Press, New York (2002)Google Scholar
  19. 19.
    Haddad, G., Leavens, G.T.: Extensible Dynamic Analysis for JML: A Case Study with Loop Annotations, University of Central Florida CS-TR-08-05 (April 2008)Google Scholar
  20. 20.
    Leavens, G.T.: The Java Modeling Language (JML) (2007),
  21. 21.
    Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P.: JML Reference Manual (2007),
  22. 22.
    Robby, P.C., Cok, D.R., Leavens, G.T.: An Evaluation of The Eclipse Java Development Tools (JDT) as a Foundational Basis for JML Reloaded (2008), jmlspecs.svn/reloaded/planning
  23. 23.
    Schirmer, N.: A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment. In: Isabelle Archive of Formal Proofs (2008)Google Scholar
  24. 24.
    Taylor, K.B.: A specification language design for the Java Modeling Language (JML) using Java 5 annotations. Masters thesis, Iowa State University (2008)Google Scholar
  25. 25.
    van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  26. 26.
    Wilson, T., Maharaj, S., Clark, R.G.: Omnibus: A Clean Language and Supporting Tool for Integrating Different Assertion-Based Verification Techniques. In: Proceedings of the Proceedings of REFT 2005, Newcastle, UK (July 2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Patrice Chalin
    • 1
  • Perry R. James
    • 1
  • George Karabotsos
    • 1
  1. 1.Dependable Software Research Group, Dept. of Computer Science and Software EngineeringConcordia UniversityMontréalCanada

Personalised recommendations