Skip to main content
SpringerLink
Log in

Generating Specifications for Recursive Methods by Abstracting Program States

  • Conference paper
  • First Online:
Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9409))

Abstract

In this paper we present a novel approach to automatically generate sound specifications for recursive methods. These specifications can help prove the absence of undesired behavior, provide programmers with a foundation to build upon and help locate implementation bugs. Our approach is based on symbolic execution which we use to determine the states of re-entry and exit points. From these we generalize the necessary pre- and postconditions using techniques from abstract interpretation. The presented approach has been prototypically implemented by integration into a faithful and precise program logic for sequential Java programs.

The work has been funded by the DFG priority program 1496 Reliably Secure Software Systems.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th Symposium on Principles of Programming Languages (POPL), pp. 238–252. ACM (1977)

    Google Scholar 

  2. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer aided verification, pp. 154–169. Springer (2000)

    Google Scholar 

  3. Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: 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 

  4. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using gröbner bases. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 2004, pp. 318–329. ACM (2004)

    Google Scholar 

  5. Furia, C.A., Meyer, B.: Inferring loop invariants using postconditions. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Fields of Logic and Computation. LNCS, vol. 6300, pp. 277–300. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1–3), 35–45 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  7. Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 260. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL 2002, pp. 58–70. ACM (2002)

    Google Scholar 

  9. La Torre, S., Parthasarathy, M., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2009, pp. 211–222. ACM (2009)

    Google Scholar 

  10. Bubel, R., Hähnle, R., Weiß, B.: Abstract interpretation of symbolic execution with explicit state updates. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 247–277. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  11. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  12. Rümmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 422–436. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S., Jones, N., (eds.) Program Flow Analysis: Theory and Applications. pp.189–233, Prentice-Hall (1981)

    Google Scholar 

  14. Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, pp. 113–130. Springer (2000)

    Google Scholar 

  15. Chen, Y.-F., Hsieh, C., Tsai, M.-H., Wang, B.-Y., Wang, F.: Verifying recursive programs using intraprocedural analyzers. In: Müller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 118–133. Springer, Heidelberg (2014)

    Google Scholar 

  16. Flanagan, C., M. Leino, K.R.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, p. 500. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Xie, Y., Aiken, A.: Saturn: A scalable framework for error detection using boolean satisfiability. ACM Trans. Program. Lang. Syst. 29(3), May 2007

    Google Scholar 

  18. Wasser, N., Bubel, R., Hähnle, R.: Array abstraction with symbolic pivots. Technical report, Department of Computer Science, Technische Universität Darmstadt, Germany August 2015. URL: https://www.se.tu-darmstadt.de/fileadmin/user_upload/Group_SE/Publications/ALBIA/TR_Symbolic_Pivots.pdf

  19. Hentschel, M., Käsdorf, S., Hähnle, R., Bubel, R.: An interactive verification tool meets an IDE. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 55–70. Springer, Heidelberg (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, TU Darmstadt, Darmstadt, Germany

    Nathan Wasser

Authors
  1. Nathan Wasser
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nathan Wasser .

Editor information

Editors and Affiliations

  1. Nanjing University, Nanjing, Jiangsu, China

    Xuandong Li

  2. Birmingham City University, Birmingham, United Kingdom

    Zhiming Liu

  3. Uppsala University, Uppsala, Sweden

    Wang Yi

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Wasser, N. (2015). Generating Specifications for Recursive Methods by Abstracting Program States. In: Li, X., Liu, Z., Yi, W. (eds) Dependable Software Engineering: Theories, Tools, and Applications. SETTA 2015. Lecture Notes in Computer Science(), vol 9409. Springer, Cham. https://doi.org/10.1007/978-3-319-25942-0_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-25942-0_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-25941-3

  • Online ISBN: 978-3-319-25942-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation