Java Program Verification Challenges

  • Bart Jacobs
  • Joseph Kiniry
  • Martijn Warnier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2852)


This paper aims to raise the level of verification challenges by presenting a collection of sequential Java programs with correctness annotations formulated in JML. The emphasis lies more on the underlying semantical issues than on verification.


Smart Card Java Program Proof Obligation Integral Type Java Modeling Language 
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.
    Ábraham Mumm, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: A Tool-supported Proof System for Multithreaded Java. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 1–32. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    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. Technical Report 2003-5, Chalmers and Göteborg University (2003),
  3. 3.
    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
  4. 4.
    Bergstra, J., Loots, M.: Empirical semantics for object-oriented programs. Artificial Intelligence Preprint Series nr. 007, Dep. Philosophy, Utrecht Univ. (1999),
  5. 5.
    Börger, E., Schulte, W.: Initialization problems in Java. Software—Concepts and Tools 20(4) (1999)Google Scholar
  6. 6.
    Burdy, L., Lanet, J.-L., Requet, A.: JACK (Java Applet Correctness Kit) (2002),
  7. 7.
    Chalin, P.: Back to basics: Language support and semantics of basic infinite integer types in JML and Larch. Technical Report, 003.1, Computer Science Department, Concordia University (2002),
  8. 8.
    Chalin, P.: Improving JML: For a safer and more effective language. Technical Report 2003-001.1, Computer Science Department, Concordia University (March 2003)Google Scholar
  9. 9.
    Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Arabnia, H.R., Mun, Y. (eds.) International Conference on Software Engineering Research and Practice (SERP 2002), pp. 322–328. CSREA Press, Las Vegas (2002)Google Scholar
  10. 10.
    Contejean, E., Duprat, J., Filliâtre, J.-C., Marché, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for JML/Java program certification (October 2002), Available via the Krakatoa home page at
  11. 11.
    Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  12. 12.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). SIGPLAN Notices, vol. 37(5), pp. 234–245. ACM, New York (2002)CrossRefGoogle Scholar
  13. 13.
    Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. The Java Series. Addison-Wesley, Reading (2000), Google Scholar
  14. 14.
    Gries, D.: The Science of Programming. Springer, Heidelberg (1981)zbMATHGoogle Scholar
  15. 15.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580, 583 (1969)zbMATHCrossRefGoogle Scholar
  16. 16.
    Huisman, M., Jacobs, B.: Inheritance in higher order logic: Modeling and reasoning. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 301–319. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  17. 17.
    Jacobs, B.: A formalisation of Java’s exception mechanism. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 284–301. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. 18.
    Jacobs, B.: Java’s integral types in PVS (2003) (manuscript),
  19. 19.
    Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B. (eds.) Behavioral Specifications of Business and Systems, pp. 175–188. Kluwer, Dordrecht (1999)Google Scholar
  20. 20.
    Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Techn. Rep. 98-06, Dep. of Comp. Sci., Iowa State Univ. (1999),
  21. 21.
    Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C.: JML reference manual, draft (2002),
  22. 22.
    Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. on Prog. Lang. & Syst. 7(16(6), 1811–1841 (1994)CrossRefGoogle Scholar
  23. 23.
    Meyer, J., Poetzsch-Heffter, A.: An architecture for interactive program provers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 63–77. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  24. 24.
    Poll, E., van den Berg, J., Jacobs, B.: Specification of the JavaCard API in JML. In: Domingo-Ferrer, J., Chan, D., Watson, A. (eds.) Smart Card Research and Advanced Application, pp. 135–154. Kluwer Acad. Publ., Dordrecht (2000)Google Scholar
  25. 25.
    Szyperski, C.: Component Software. Addison-Wesley, Reading (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Bart Jacobs
    • 1
  • Joseph Kiniry
    • 1
  • Martijn Warnier
    • 1
  1. 1.Dep. Comp. Sci.Univ. NijmegenNijmegenThe Netherlands

Personalised recommendations