Skip to main content
SpringerLink
Log in

Refining Abstract Interpretation-Based Static Analyses with Hints

  • Conference paper
Programming Languages and Systems (APLAS 2009)

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

Included in the following conference series:

Abstract

We focus our attention on the loss of precision induced by abstract domain operations. We introduce a new technique, hints, which allows us to systematically refine the operations defined over elements of an abstract domain. We formally define hints in the abstract interpretation theory, we prove their soundness, and we characterize two families of hints: syntactic and semantic. We give some examples of hints, and we provide our experience with hints in Clousot, our abstract interpretation-based static analyzer for .NET.

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. Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 135–148. Springer, Heidelberg (2004)

    Google Scholar 

  2. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI 2003. ACM Press, New York (2003)

    Google Scholar 

  3. Colby, C., Lee, P.: Trace-based program analysis. In: POPL 1996. ACM Press, New York (1996)

    Google Scholar 

  4. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977 (1977)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  6. Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4) (August 1992)

    Google Scholar 

  7. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Combination of abstractions in the ASTRÉE static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

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

    Google Scholar 

  9. Das, M., Lerner, S., Seigle, M.: Esp: Path-sensitive program verification in polynomial time. In: PLDI 2002, pp. 57–68 (2002)

    Google Scholar 

  10. Ferrara, P., Logozzo, F., Fähndrich, M.A.: Safer unsafe code in.Net. In: OOPSLA 2008 (2008)

    Google Scholar 

  11. Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 144–160. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  12. Gopan, D., Reps, T.W.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452–466. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Granger, P.: Improving the results of static analyses programs by local decreasing iteration. In: Shyamasundar, R.K. (ed.) FSTTCS 1992. LNCS, vol. 652. Springer, Heidelberg (1992)

    Google Scholar 

  14. Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 443–458. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  15. Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL 2008. ACM Press, New York (2008)

    Google Scholar 

  16. Handjieva, M., Tzolovski, S.: Refining static analyses by trace-based partitioning using control flow. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 200–214. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  17. Laviron, V., Logozzo, F.: Subpolyhedra: a (more) scalable approach to infer linear inequalities. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 229–244. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  18. Logozzo, F., Fähndrich, M.A.: Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. In: SAC 2008 (2008)

    Google Scholar 

  19. Manevich, R., Field, J., Henzinger, T.A., Ramalingam, G., Sagiv, M.: Abstract counterexample-based refinement for powerset domains. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol. 4444, pp. 273–292. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  20. Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)

    Google Scholar 

  21. Microsoft. Codecontracts tools, http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx

  22. Microsoft. Contracts namespace, http://msdn.microsoft.com/en-us/library/~system.diagnostics.contractsVS.100.aspx

  23. Miné, A.: The octagon abstract domain. In: WCRE 2001 (2001)

    Google Scholar 

  24. Monniaux, D.: Automatic modular abstractions for linear constraints. In: POPL 2009 (2009)

    Google Scholar 

  25. Péron, M., Halbwachs, N.: An abstract domain extending difference-bound matrices with disequality constraints. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 268–282. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Yorsh, G., Reps, T.W., Sagiv, S.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530–545. Springer, Heidelberg (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. École Normale Supérieure, 45, rue d’Ulm, Paris, France

    Vincent Laviron

  2. Microsoft Research, Redmond, WA, USA

    Francesco Logozzo

Authors
  1. Vincent Laviron
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Francesco Logozzo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. National Institute of Informatics (NII), Information Systems Architecture REsearch Division, 2-1-2 Hitotsubashi, Chiyoda-ku, 101-8430, Tokyo, Japan

    Zhenjiang Hu

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Laviron, V., Logozzo, F. (2009). Refining Abstract Interpretation-Based Static Analyses with Hints. In: Hu, Z. (eds) Programming Languages and Systems. APLAS 2009. Lecture Notes in Computer Science, vol 5904. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10672-9_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-10672-9_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-10671-2

  • Online ISBN: 978-3-642-10672-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation