Skip to main content
SpringerLink
Log in
Book cover

International SPIN Workshop on Model Checking of Software

SPIN 2004: Model Checking Software pp 164–181Cite as

Verification of Java Programs Using Symbolic Execution and Invariant Generation

  • Conference paper

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

Abstract

Software verification is recognized as an important and difficult problem. We present a novel framework, based on symbolic execution, for the automated verification of software. The framework uses annotations in the form of method specifications and loop invariants. We present a novel iterative technique that uses invariant strengthening and approximation for discovering these loop invariants automatically. The technique handles different types of data (e.g. boolean and numeric constraints, dynamically allocated structures and arrays) and it allows for checking universally quantified formulas. Our framework is built on top of the Java PathFinder model checking toolset and it was used for the verification of several non-trivial Java programs.

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. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: Proc. PLDI, pp. 203–213 (2001)

    Google Scholar 

  2. Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 158. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  3. Bensalem, S., Lakhnech, Y., Saidi, H.: Powerful techniques for the automatic generation of invariants. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)

    Google Scholar 

  4. Bjorner, N., Browne, A., Colon, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.: Verifying temporal properties of reactive systems: A STeP tutorial. FMSD 16, 227–270 (2000)

    Google Scholar 

  5. Colon, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  6. Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Păsăreanu, C., Robby, Zheng, H.: Bandera : Extracting finite-state models from Java source code. In: Proc. ICSE 2000 (2000)

    Google Scholar 

  7. Cousot, P., Cousot, R.: On abstraction in software verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 37. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. 5th POPL (1978)

    Google Scholar 

  9. Delzanno, G., Podelski, A.: Widen, narrow and relax. Technical report

    Google Scholar 

  10. Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (1998)

    Google Scholar 

  11. Dor, N., Rodeh, M., Sagiv, M.: Checking cleanness in linked lists. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 115–135. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  12. Ernst, M.D., Czeisler, A., Griswold, W.G., Notkin, D.: Quickly detecting relevant program invariants. In: Proc. ICSE. ACM (2000)

    Google Scholar 

  13. Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proc. POPL (2002)

    Google Scholar 

  14. Floyd, R.W.: Assigning meanings to programs. In: Proc. Symposia in Applied Mathematics, vol. 19, pp. 19–32 (1967)

    Google Scholar 

  15. Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proc. POPL, pp. 174–186, Paris, France (January 1997)

    Google Scholar 

  16. Graf, S., Saidi, H.: Verifying invariants using theorem proving. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 196–207. Springer, Heidelberg (1996)

    Google Scholar 

  17. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Google Scholar 

  18. Hantler, S.L., King, J.C.: An introduction to proving the correctness of programs. ACM Comput. Surv. 8(3), 331–353 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  19. Havelund, K., Shankar, N.: Experiments in theorem proving and model checking for protocol verification. In: Gaudel, M.-C., Woodcock, J.C.P. (eds.) FME 1996. LNCS, vol. 1051, pp. 662–681. Springer, Heidelberg (1996)

    Google Scholar 

  20. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  21. Holzmann, G.: The Spin Model Checker: Primer and Reference Manual (2003)

    Google Scholar 

  22. Karr, M.: Affine relationships among variables of a program. Acta Informatica 6 (1976)

    Google Scholar 

  23. Khurshid, S., Păsăreanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  24. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MATH  Google Scholar 

  25. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification (1992)

    Google Scholar 

  26. Moeller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Proc. PLDI, Snowbird, UT (June 2001)

    Google Scholar 

  27. Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM 31(8) (August 1992)

    Google Scholar 

  28. Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Trans. Prog. Lang. Syst. (January 1998)

    Google Scholar 

  29. Tiwari, A., Rues, H., Saidi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 113. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  30. Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proc. ASE, Grenoble, France (2000)

    Google Scholar 

  31. Wegbreit, B.: The synthesis of loop predicates. Communications of the ACM 17(2), 102–112 (1974)

    Article  MATH  MathSciNet  Google Scholar 

  32. Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 88–97. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  33. Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, p. 69. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Kestrel Technology, NASA Ames Research Center, Moffett Field, CA, 94035, USA

    Corina S. Păsăreanu

  2. RIACS/USRA, NASA Ames Research Center, Moffett Field, CA, 94035, USA

    Willem Visser

Authors
  1. Corina S. Păsăreanu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Willem Visser
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. VERIMAG, 2 Avenue de Vignate, Centre Equitation, 38610, Grenoble-Gières, France

    Susanne Graf

  2. Vérimag Laboratory, 2 avenue de Vignate, 38610, Gières, France

    Laurent Mounier

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Păsăreanu, C.S., Visser, W. (2004). Verification of Java Programs Using Symbolic Execution and Invariant Generation. In: Graf, S., Mounier, L. (eds) Model Checking Software. SPIN 2004. Lecture Notes in Computer Science, vol 2989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24732-6_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24732-6_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-21314-7

  • Online ISBN: 978-3-540-24732-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation