Skip to main content
SpringerLink
Log in

Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs

  • Conference paper
Algebraic Methodology and Software Technology (AMAST 2004)

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

Abstract

We propose a new approach to interprocedural analysis and verification, consisting of deriving an interprocedural analysis method by abstract interpretation of the standard operational semantics of programs. The advantages of this approach are twofold. From a methodological point of view, it provides a direct connection between the concrete semantics of the program and the effective analysis, which facilitates implementation and correctness proofs. This method also integrates two main, distinct methods for interprocedural analysis, namely the call-string and the functional approaches introduced by Sharir and Pnueli. This enables strictly more precise analyses and additional flexibility in the tradeoff between efficiency and precision of the analysis.

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. Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL 2003, pp. 62–73. ACM, New York (2003)

    Chapter  Google Scholar 

  3. Bourdoncle, F.: Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity. In: Deransart, P., Małuszyński, J. (eds.) PLILP 1990. LNCS, vol. 456, pp. 307–323. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  4. Bourdoncle, F.: Assertion-based debugging of imperative programs by abstract interpretation. In: Sommerville, I., Paul, M. (eds.) ESEC 1993. LNCS, vol. 717, pp. 501–516. Springer, Heidelberg (1993)

    Google Scholar 

  5. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238–252. ACM, New York (1977)

    Chapter  Google Scholar 

  6. Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Formal Description of Programming Concepts, pp. 237–277. North Holland, Amsterdam (1977)

    Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming 13(2–3) (1992)

    Google Scholar 

  8. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, pp. 84–97. ACM, New York (1978)

    Chapter  Google Scholar 

  9. Creusillet, B., Irigoin, F.: Interprocedural array region analyses. International Journal of Parallel Programming, 24(6) (1996)

    Google Scholar 

  10. Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: PLDI 1994, pp. 230–241. ACM, New York (1994)

    Chapter  Google Scholar 

  11. Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural dataflow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 14–30. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. Feret, J.: Abstract interpretation-based static analysis of mobile ambients. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 412–430. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  14. Gaucher, F., Jahier, E., Jeannet, B., Maraninchi, F.: Automatic state reaching for debugging reactive programs. In: AADEBUG 2003 (2003)

    Google Scholar 

  15. Jeannet, B.: Dynamic partitioning in linear relation analysis. Application to the verification of reactive systems. Formal Methods in System Design, 23(1) (2003)

    Google Scholar 

  16. Jeannet, B., Serwe, W.: Abstracting call-stacks for interprocedural verification of imperative programs. Research Report 4904, INRIA (July 2003)

    Google Scholar 

  17. Jensen, T., Spoto, F.: Class analysis of object-oriented programs through abstract interpretation. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 261–275. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: POPL 1982, ACM, New York (1982)

    Google Scholar 

  19. Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol. 641, pp. 125–140. Springer, Heidelberg (1992)

    Google Scholar 

  20. Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, pp. 310–319. IEEE, Los Alamitos (2001)

    Google Scholar 

  21. Nielson, F.: Tensor products generalize the relational data flow analysis method. In: 4th Hungarian Computer Science Conference (1985)

    Google Scholar 

  22. Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL 1995, pp. 49–61. ACM, New York (1995)

    Chapter  Google Scholar 

  23. Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  24. Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 133–149. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  25. Rusu, V., du Bousquet, L., Jéron, T.: An approach to symbolic test generation. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 338–357. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  26. Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. TCS 167(1–2), 131–170 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  27. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM ToPLaS 24(3) (2002)

    Google Scholar 

  28. Sharir, M., Pnueli, A.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications. ch.7, Prentice Hall, Englewood Cliffs (1981)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRISA, 35042, Rennes, France

    Bertrand Jeannet

  2. INRIA Rhône-Alpes, 38334, St Ismier, France

    Wendelin Serwe

Authors
  1. Bertrand Jeannet
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wendelin Serwe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Stirling, FK9 4LA, Stirling, UK

    Charles Rattray

  2. University of Stirling, FK9 4LA, Stirling

    Savitri Maharaj

  3. Department of Computing Science and Mathematics, University of Stirling, FK9 4LA, Stirling, UK

    Carron Shankland

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jeannet, B., Serwe, W. (2004). Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs. In: Rattray, C., Maharaj, S., Shankland, C. (eds) Algebraic Methodology and Software Technology. AMAST 2004. Lecture Notes in Computer Science, vol 3116. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27815-3_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27815-3_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22381-8

  • Online ISBN: 978-3-540-27815-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation