Advertisement

Integrating Tools for Automatic Program Verification

  • Engelbert Hubbers
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2890)

Abstract

In this paper we describe our findings after integrating several tools based upon the Java Modeling Language (JML) [1], a specification language used to annotate Java programs. The tools we consider are Daikon [2], ESC/Java [3], JML runtime assertion checker [1], and Loop/PVS tool [4]. The first one generates specifications; the others are used to verify them. We find that for the first three it is worthwhile to combine them because this is relatively easy and it improves the specifications. Combining Daikon and the Loop/PVS tool directly works in theory, but in practice it only works if the test suite is very good and hence it is not advisable.

Keywords

Test Suite Automatic Program Java Modeling Language Assertion Violation Runtime Check 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report 98-06t, Iowa State University, Dep. of Computer Science (2002), See http://www.jmlspecs.org
  2. 2.
    Ernst, M., Cockrell, J., Griswold, W., Notkin, D.: Dynamically Discovering Likely Program Invariants to Support Program Evolution. IEEE Trans. on Software Eng. 27, 99–123 (2001)CrossRefGoogle Scholar
  3. 3.
    Compaq Systems Research Center: Extended Static Checker for Java, version 1.2.4 (2001), http://research.compaq.com/SRC/esc/
  4. 4.
    Nijmeegs Instituut voor Informatica en Informatiekunde, University of Nijmegen, The Netherlands: Security of Systems group (2003), http://www.cs.kun.nl/ita/research/projects/loop/
  5. 5.
    Hoare, T.: The verifying compiler: a grand challenge for computing research. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 1–12. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Lab. for Computer Science, MIT: Daikon Invariant Detector, version 2.4.2 (2003), http://pag.lcs.mit.edu/daikon/
  8. 8.
    Burdy, L., Lanet, J.-L., Requet, A.: JACK (Java Applet Correctness Kit) (2002), http://www.gemplus.com/smart/r_d/trends/jack.html
  9. 9.
    Cataño, N., Huisman, M.: Chase: A Static checker for JML’s Assignable Clause. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 26–40. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Meyer, B.: Eiffel: the language. Prentice Hall, New York (1992)zbMATHGoogle Scholar
  11. 11.
    Nimmer, J.W., Ernst, M.D.: Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. In: Havelund, K., Rosu, G. (eds.) Electronic Notes in Theoretical Computer Science, vol. 55. Elsevier Science Publishers, Amsterdam (2001)Google Scholar
  12. 12.
    Nimmer, J.W., Ernst, M.D.: Automatic generation of program specifications. In: ISSTA 2002, Proceedings of the 2002 International Symposium on Software Testing and Analysis, Rome, Italy, pp. 232–242 (2002)Google Scholar
  13. 13.
    Win, T.N., Ernst, M.D.: Verifying distributed algorithms via dynamic analysis and theorem proving. Technical Report 841, MIT Lab. for Computer Science (2002)Google Scholar
  14. 14.
    Garland, S.J., Guttag, J.V.: A guide to LP, the Larch Prover. Technical Report 82, Digital Equipment Corporation, Systems Research Center (1991)Google Scholar
  15. 15.
    Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Software 19, 42–51 (2002)CrossRefGoogle Scholar
  16. 16.
    Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  17. 17.
    Leavens, G., et al.: Java Modeling Language, JML (2003), http://www.jmlspecs.org/
  18. 18.
    Computer Science Lab., SRI: The PVS Specification and Verification System, version 2.4.1 (2002), http://pvs.csl.sri.com
  19. 19.
    Weiss, M.A.: Data Structures and Algorithm Analysis in Java. Addison Wesley, Reading (1999) ISBN: 0-201-35754-2Google Scholar
  20. 20.
    Jacobs, B.P.: A Tutorial for the Logic of JML in PVS. under development (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Engelbert Hubbers
    • 1
  1. 1.Nijmeegs Instituut voor Informatica en InformatiekundeUniversity of NijmegenNijmegenThe Netherlands

Personalised recommendations