Skip to main content
SpringerLink
Log in

A Generic Framework for Interprocedural Analysis of Numerical Properties

  • Conference paper
Static Analysis (SAS 2005)

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

Included in the following conference series:

Abstract

In his seminal paper [5], Granger presents an analysis which infers linear congruence relations between integer variables. For affine programs without guards, his analysis is complete, i.e., infers all such congruences. No upper complexity bound, though, has been found for Granger’s algorithm. Here, we present a variation of this analysis which runs in polynomial time. Moreover, we provide an interprocedural extension of this algorithm. These algorithms are obtained by means of multiple instances of a general framework for constructing interprocedural analyses of numerical properties. Finally, we indicate how the analyses can be enhanced to deal with equality guards interprocedurally.

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. Balakrishnan, G., Reps, T.W.: Analyzing Memory Accesses in x86 Executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 5–23. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgue, C., Mormiaux, D., Rival, X.: A Static Analyzer for Large Safety-Critical Software. In: Int. ACM Conf. on Programming Language Design and Implementation (PLDI), pp. 196–207 (2003)

    Google Scholar 

  3. Dor, N., Rodeh, M., Sagiv, M.: Cleanness checking of string manipulations in C programs via integer analysis. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 194–212. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Granger, P.: Static Analysis of Arithmetical Congruences. Int. J. of Computer Math., 165–190 (1989)

    Google Scholar 

  5. Granger, P.: Static Analysis of Linear Congruence Equalities among Variables of a Program. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493, pp. 169–192. Springer, Heidelberg (1991)

    Google Scholar 

  6. Gulwani, S., Necula, G.: Discovering Affine Equalities Using Random Interpretation. In: 30th ACM Symp. on Principles of Programming Languages (POPL), pp. 74–84 (2003)

    Google Scholar 

  7. Gulwani, S., Necula, G.: Precise Interprocedural Analysis Using Random Interpretation. In: 32th Ann. ACM Symp. on Principles of Programming Languages (POPL), pp. 324–337 (2005)

    Google Scholar 

  8. Hafner, J., McCurley, K.: Asymptotically Fast Triangularization of Matrices over Rings. SIAM J. of Computing 20(6), 1068–1083 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  9. Karr, M.: Affine Relationships Among Variables of a Program. Acta Informatica 6, 133–151 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  10. Lang, S.: Algebra, 3rd edn. Pearson Education, Inc., London (1993)

    MATH  Google Scholar 

  11. Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Müller-Olm, M., Seidl, H.: A note on karr’s algorithm. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 1016–1028. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  13. Müller-Olm, M., Seidl, H.: Precise Interprocedural Analysis through Linear Algebra. In: 31st ACM Symp. on Principles of Programming Languages (POPL), pp. 330–341 (2004)

    Google Scholar 

  14. Müller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 46–60. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  15. Simon, A., King, A.: Analyzing string buffers in C. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 365–379. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  16. Storjohann, A.: Algorithms for Matrix Canonical Forms. PhD thesis, ETH Zürich, Diss. ETH No. 13922 (2000)

    Google Scholar 

  17. Storjohann, A.: A Fast, Practical, and Deterministic Algorithm for Triangularizing Integer Matrices. Tech. Rep. 255, ETH Zürich (1996)

    Google Scholar 

  18. Zariski, O., Samuel, P.: Commutative Algebra, Nostrand, Princeton, NJ, vol. I (1958)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, LS 5, Universität Dortmund, Baroper Str. 301, 44221, Dortmund, Germany

    Markus Müller-Olm

  2. Institut für Informatik, I2, TU München, 80333, München, Germany

    Helmut Seidl

Authors
  1. Markus Müller-Olm
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Helmut Seidl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Imperial College London,  

    Chris Hankin

  2. Department of Computing, Imperial College London, 180 Queen’s Gate, SW7 2BZ, London, UK

    Igor Siveroni

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Müller-Olm, M., Seidl, H. (2005). A Generic Framework for Interprocedural Analysis of Numerical Properties. In: Hankin, C., Siveroni, I. (eds) Static Analysis. SAS 2005. Lecture Notes in Computer Science, vol 3672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11547662_17

Download citation

  • DOI: https://doi.org/10.1007/11547662_17

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-31971-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation