Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Software Security

ISSS 2003: Software Security - Theories and Systems pp 134–153Cite as

Java Program Verification at Nijmegen: Developments and Perspective

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3233))

Abstract

This paper presents a historical overview of the work on Java program verification at the University of Nijmegen (the Netherlands) over the past six years (1997–2003). It describes the development and use of the LOOP tool that is central in this work. Also, it gives a perspective on the field.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. van den Berg, J., Huisman, M., Jacobs, B., Poll, E.: A type-theoretic memory model for verification of sequential Java programs. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 1–21. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  3. Breunesse, C.-B., van den Berg, J., Jacobs, B.: Specifying and verifying a decimal representation in Java for smart cards. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 304–318. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Formal Methods for Industrial Critical Systems (FMICS 2003). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 80, pp. 73–89. Elsevier, Amsterdam (2003)

    Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. Y. Cheon and G.T. Leavens. A runtime assertion checker for the Java Modeling Language (JML). In Hamid R. Arabnia and Youngsong Mun, editors, the International Conference on Software Engineering Research and Practice (SERP ’02), pages 322–328. CSREA Press, 2002.

    Google Scholar 

  7. ESC/Java2. Open source extended static checking for Java version 2 (ESC/Java 2) project. Security of Systems Group, Univ. of Nijmegen, www.cs.kun.nl/ita/research/projects/sos/projects/escjava.html

  8. Ahrendt, W., et al.: The key tool. Technical report in computing science no.2003-5, Dept. of Computing Science, Chalmers University and Göteborg University, Göteborg, Sweden (2003)

    Google Scholar 

  9. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), pp. 234–245 (2002)

    Google Scholar 

  10. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. The Java Series. Addison-Wesley, Reading (2000), http://java.sun.com/docs/books/jls/second_edition/html/j.title.doc.html

    Google Scholar 

  11. Griffioen, D., Huisman, M.: A comparison of PVS and Isabelle/HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 123–142. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  12. Hensel, U.: Definition and Proof Principles for Data and Processes. PhD thesis, Techn. Univ. Dresden, Germany (1999)

    Google Scholar 

  13. Hensel, U., Huisman, M., Jacobs, B., Tews, H.: Reasoning about classes in object-oriented languages: Logical models and tools. In: Hankin, C. (ed.) ESOP 1998 and ETAPS 1998. LNCS, vol. 1381, pp. 105–121. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  14. Huisman, M.: Reasoning about JAVA Programs in higher order logic with PVS and Isabelle. PhD thesis, Univ. Nijmegen (2001)

    Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T.S.E. (ed.) ETAPS 2000 and FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  17. Jacobs, B.: Objects and classes, co-algebraically. In: Freitag, B., Jones, C.B., Lengauer, C., Schek, H.-J. (eds.) Object-Orientation with Parallelism and Persistence, pp. 83–103. Kluwer Academic Publishers, Dordrecht (1996)

    Google Scholar 

  18. Jacobs, B.: Java’s integral types in PVS. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 1–15. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  19. Jacobs, B.: Weakest precondition reasoning for Java programs with JML annotations. Journ. of Logic and Algebraic Programming 58, 61–88 (2004)

    Article  MATH  Google Scholar 

  20. Jacobs, B., Kiniry, J., Warnier, M.: Java program verification challenges. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 202–219. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  21. Jacobs, B., Oostdijk, M., Warnier, M.: Source code verification of a secure payment applet. Journ. of Logic and Algebraic Programming 58, 107–120 (2004)

    Article  MATH  Google Scholar 

  22. Jacobs, B., Poll, E.: Coalgebras and monads in the semantics of Java. Theor. Comp. Sci. 291(3), 329–349 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  23. Jacobs, B., van den Berg, J., Huisman, M., van Berkum, M., Hensel, U., Tews, H.: Reasoning about classes in Java (preliminary report). In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pp. 329–340. ACM Press, New York (1998)

    Google Scholar 

  24. 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 Academic Publishers, Dordrecht (1999)

    Google Scholar 

  25. Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 262–284. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  26. Malcolm, G.: Behavioural equivalence, bisimulation and minimal realisation. In: Haveraaen, M., Dahl, O.-J., Owe, O. (eds.) Abstract Data Types 1995 and COMPASS 1995. LNCS, vol. 1130, pp. 359–378. Springer, Heidelberg (1996)

    Google Scholar 

  27. Marché, C., Paulin, C., Urbain, X.: The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML. Journ. of Logic and Algebraic Programming 58, 89–106 (2004)

    Article  MATH  Google Scholar 

  28. Meyer, J., Poetzsch-Heffter, A.: An architecture for interactive program provers. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol. 1785, pp. 63–77. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  29. Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular specification of frame properties in JML. Concurrency and Computation: Practice and Experience 15(2), 117–154 (2003)

    Article  MATH  Google Scholar 

  30. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  31. von Oheimb, D., Nipkow, T.: Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 89–105. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  32. Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996)

    Google Scholar 

  33. Poll, E., van den Berg, J., Jacobs, B.: Formal specification of the JavaCard API in JML: the APDU class. Computer Networks 36(4), 407–421 (2001)

    Article  Google Scholar 

  34. Reichel, H.: An approach to object semantics based on terminal co-algebras. Math. Struct. in Comp. Sci. 5, 129–152 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  35. Rothe, J., Tews, H., Jacobs, B.: The coalgebraic class specification language CCSL. Journ. of Universal Comp. Sci. 7(2) (2001)

    Google Scholar 

  36. Tews, H.: Coalgebraic Methods for Object-Oriented Specification. PhD thesis, Techn. Univ. Dresden, Germany (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Nijmegen, P.O. Box 9010, 6500 GL, Nijmegen, The Netherlands

    Bart Jacobs & Erik Poll

Authors
  1. Bart Jacobs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Erik Poll
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Japan Advanced Institute of Science and Technology, (JAIST),  

    Kokichi Futatsugi

  2. Faculty of Science and Technology, Tokyo University of Science, Yamazaki 2641, Noda, Chiba, Japan

    Fumio Mizoguchi

  3. Tokyo Institute of Technology,  

    Naoki Yonezaki

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jacobs, B., Poll, E. (2004). Java Program Verification at Nijmegen: Developments and Perspective. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds) Software Security - Theories and Systems. ISSS 2003. Lecture Notes in Computer Science, vol 3233. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-37621-7_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-37621-7_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23635-1

  • Online ISBN: 978-3-540-37621-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation