Skip to main content
SpringerLink
Log in

On the Utility of Canonical Abstraction

  • Conference paper
Engineering Theories of Software Intensive Systems

Part of the book series: NATO Science Series ((NAII,volume 195))

  • 379 Accesses

Abstract

Abstraction and abstract interpretation are key tools for automatically verifying properties of systems. One of the major challenges in abstract interpretation is how to obtain abstractions that are precise enough to provide useful information, and yet abstract enough to allow efficient computation. A related challenge is how to conservatively extract useful information from an abstract value.

This is a survey paper on a parametric abstract domain called canonical abstraction, which was motivated by the problem of shape analysis — i.e., the problem of determining “shape invariants” for programs that perform destructive updating on dynamically allocated storage.

We discuss three conservative methods from extracting information from abstract values: the first method is obtained using the Kleene interpretation of the query formula; this method is simple and very efficient, but is not very precise. The second method is the most precise, but requires the use of a theorem prover. The third method achieves precision close to the second method with tolerable costs, but requires some additional information from the designers of the abstraction.

We discuss the canonical-abstraction domain, and show the properties of programs that have been verified by the domain.

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 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover 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. TVLA system. “http://www.cs.tau.ac.il/~TVLA/”.

    Google Scholar 

  2. Andersen, L. O. (1993). Binding-time analysis and the taming of C pointers. In Part. Eval. and Semantics-Based Prog. Manip., pages 47–58.

    Google Scholar 

  3. Arnold, G. (2004). Combining heap analyses by intersecting abstractions. Master’s thesis, Tel Aviv University.

    Google Scholar 

  4. Ball, T., Majumdar, R., Millstein, T., and Rajamani, S. (2001). Automatic predicate abstraction of C programs. In Prog. Lang. Design and Impl., NewYork, NY. ACM Press.

    Google Scholar 

  5. Ball, T. and Rajamani, S. (2001). The SLAM toolkit. In Int. Conf. on Computer Aided Verif., volume 2102 of Lec. Notes in Comp. Sci., pages 260–264.

    Google Scholar 

  6. Bush, W., Pincus, J., and Sielaff, D. (2000). A static analyzer for finding dynamic programming errors. Software-Practice&Experience, 30:775–802.

    Google Scholar 

  7. Chase, D., Wegman, M., and Zadeck, F. (1990). Analysis of pointers and structures. In Prog. Lang. Design and Impl., pages 296–310, New York, NY. ACM Press.

    Google Scholar 

  8. Chen, H. and Wagner, D. (2002). MOPS: An infrastructure for examining security properties of software. In Conf. on Comp. and Commun. Sec., pages 235–244.

    Google Scholar 

  9. Cheng, B.-C. and Hwu, W. (2000). Modular interprocedural pointer analysis using access paths: Design, implementation, and evaluation. In Prog. Lang. Design and Impl., pages 57–69.

    Google Scholar 

  10. Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. (2000). Counterexample-guided abstraction refinement. In Int. Conf. on Computer Aided Verif., pages 154–169.

    Google Scholar 

  11. Clarke, E., Grumberg, O., and Long, D. (1994). Model checking and abstraction. Trans. on Prog. Lang. and Syst., 16(5):1512–1542.

    Google Scholar 

  12. Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Robby, and Zheng, H. (2000). Bandera: Extracting finite-state models from Java source code. In Int. Conf. on Softw. Eng., pages 439–448.

    Google Scholar 

  13. Cousot, P. and Cousot, R. (1977). Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Princ. of Prog. Lang., pages 238–252.

    Google Scholar 

  14. Cousot, P. and Cousot, R. (1979). Systematic design of program analysis frameworks. In Princ. of Prog. Lang., pages 269–282.

    Google Scholar 

  15. Das, M. (2000). Unification-based pointer analysis with directional assignments. In Prog. Lang. Design and Impl., pages 35–46.

    Google Scholar 

  16. Deutsch, A. (1994). Interprocedural may-alias analysis for pointers: Beyond k-limiting. In Prog. Lang. Design and Impl., pages 230–241, New York, NY. ACM Press.

    Google Scholar 

  17. Engler, D., Chelf, B., Chou, A., and Hallem, S. (2000). Checking system rules using system-specific, programmer-written compiler extensions. In Op. Syst. Design and Impl., pages 1–16.

    Google Scholar 

  18. Fähndrich, M., Rehof, J., and Das, M. (2000). Scalable context-sensitive flow analysis using instantiation constraints. In Prog. Lang. Design and Impl., pages 253–263.

    Google Scholar 

  19. Foster, J., Fähndrich, M., and Aiken, A. (2000). Polymorphic versus monomorphic flow-insensitive points-to analysis for C. In Static Analysis Symp., pages 175–198.

    Google Scholar 

  20. Ginsberg, M. (1988). Multivalued logics: A uniform approach to inference in artificial intelligence. Comp. Intell., 4:265–316.

    Google Scholar 

  21. Gopan, D., DiMaio, F., N. Dor, Reps, T., and Sagiv, M. (2004). Numeric domains with summarized dimensions. In Tools and Algs. for the Construct. and Anal. of Syst., pages 512–529.

    Google Scholar 

  22. Gopan, D., Reps, T., and Sagiv, M. (2005). Numeric analysis of array operations. In Princ. of Prog. Lang.

    Google Scholar 

  23. Graf, S. and Saïdi, H. (1997). Construction of abstract state graphs with PVS. In Int. Conf. on Computer Aided Verif., volume 1254 of Lec. Notes in Comp. Sci., pages 72–83.

    Google Scholar 

  24. Havelund, K. and Pressburger, T. (2000). Model checking Java programs using Java PathFinder. Softw. Tools for Tech. Transfer, 2(4).

    Google Scholar 

  25. Jeannet, B., Loginov, A., Reps, T., and Sagiv, M. (2004). A relational approach to interprocedural shape analysis. In Static Analysis Symp. Springer.

    Google Scholar 

  26. Jones, N. and Muchnick, S. (1982). A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Princ. of Prog. Lang., pages 66–74, New York, NY. ACM Press.

    Google Scholar 

  27. Landi, W. and Ryder, B. (1991). Pointer induced aliasing: A problem classification. In Princ. of Prog. Lang., pages 93–103, New York, NY. ACM Press.

    Google Scholar 

  28. Lev-Ami, T. (2000). TVLA: A framework for Kleene based static analysis. Master’s thesis, Tel-Aviv University, Tel-Aviv, Israel.

    Google Scholar 

  29. Lev-Ami, T., Reps, T., Sagiv, M., and Wilhelm, R. (2000). Putting static analysis to work for verification: A case study. In Int. Symp. on Softw. Testing and Analysis, pages 26–38.

    Google Scholar 

  30. Lev-Ami, T. and Sagiv, M. (2000). TVLA: A system for implementing static analyses. In Static Analysis Symp., pages 280–301.

    Google Scholar 

  31. Loginov, A., Reps, T., and Sagiv, M. (2004). Abstraction refinement for 3-valued-logic analysis. Submitted for publication.

    Google Scholar 

  32. Manevich, R., Ramalingam, G., Field, J., Goyal, D., and Sagiv, M. (2002). Compactly representing first-order structures for static analysis. In Static Analysis Symp., pages 196–212.

    Google Scholar 

  33. Manevich, R., Sagiv, M., Ramalingam, G., and Field, J. (2004). Partially disjunctive heap abstraction. In Proceedings of the 11th International Symposium, SAS 2004, volume 3148 of Lecture Notes in Computer Science, pages 265–279. Springer.

    MathSciNet  Google Scholar 

  34. Manevich, R., Yahav, E., Ramalingam, G., and Sagiv, M. (2005). Predicate abstraction and canonical abstraction for singly-linked lists. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation, VMCAI 2005, Lecture Notes in Computer Science. Springer.

    Google Scholar 

  35. M. Das, Liblit, B., Fähndrich, M., and Rehof, J. (2001). Estimating the impact of scalable pointer analysis on optimization. In Static Analysis Symp., pages 260–278.

    Google Scholar 

  36. Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., and Sagiv, M. (2002). Deriving specialized program analyses for certifying component-client conformance. In Prog. Lang. Design and Impl., pages 83–94.

    Google Scholar 

  37. Reps, T., Sagiv, M., and Loginov, A. (2003). Finite differencing of logical formulas for static analysis. In European Symp. On Programming, pages 380–398.

    Google Scholar 

  38. Rinetskey, N. and Sagiv, M. (2001). Interprocedural shape analysis for recursive programs. In Wilhelm, R., editor, Comp. Construct., volume 2027 of LNCS, pages 133–149. Springer-Verlag.

    Google Scholar 

  39. Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., and Wilhelm, R. (2005). A semantics for procedure local heaps and its abstractions. In Princ. of Prog. Lang.

    Google Scholar 

  40. Rinetzky, N., Sagiv, M., and Yahav, E. (2004). Computing procedure summaries exploiting heap-locality. Tech. Rep. XXX, Tel Aviv Uni. Available at “http://www.cs.tau.ac.il/~maon”.

    Google Scholar 

  41. Sagiv, M., Reps, T., and Wilhelm, R. (1998). Solving shape-analysis problems in languages with destructive updating. Trans. on Prog. Lang. and Syst., 20(1):1–50.

    Google Scholar 

  42. Sagiv, M., Reps, T., and Wilhelm, R. (2002). Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst., 24(3):217–298.

    Google Scholar 

  43. Shaham, R., Yahav, E., Kolodner, E., and Sagiv, M. (2003). Establishing local temporal heap safety properties with applications to compile-time memory management. In Proc. of Static Analysis Symposium (SAS’03), volume 2694 of LNCS, pages 483–503. Springer.

    MathSciNet  Google Scholar 

  44. Steensgaard, B. (1996). Points-to analysis in almost-linear time. In Princ. of Prog. Lang., pages 32–41.

    Google Scholar 

  45. Wagner, D., Foster, J., Brewer, E., and Aiken, A. (2000). A first step towards automated detection of buffer overrun vulnerabilities. In Network and Dist. Syst. Security.

    Google Scholar 

  46. Whaley, J. and Lam, M. (2004). Cloning-based context-sensitive pointer alias analyses using binary decision diagrams. In Prog. Lang. Design and Impl.

    Google Scholar 

  47. Yahav, E. (2001). Verifying safety properties of concurrent Java programs using 3-valued logic. In Princ. of Prog. Lang., pages 27–40.

    Google Scholar 

  48. Yahav, E. and Ramalingam, G. (2004). Verifying safety properties using separation and heterogeneous abstractions. In Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, pages 25–34. ACM Press.

    Google Scholar 

  49. Yahav, E., Reps, T., Sagiv, M., and Wilhelm, R. (2003). Verifying temporal heap properties specified via evolution logic. In Proc. of the 12th European Symposium on Programming, ESOP 2003, volume 2618 of LNCS.

    Google Scholar 

  50. Yahav, E. and Sagiv, M. (2003). Automatically verifying concurrent queue algorithms. In Workshop on Software Model Checking.

    Google Scholar 

  51. 2003] Yorsh, G. (2003). Logical characterizations of heap abstractions. Master’s thesis, Tel Aviv University.

    Google Scholar 

  52. Yorsh, G., Reps, T., and Sagiv, M. (2004). Symbolically computing most-precise abstract operations for shape analysis. In Tools and Algs. for the Construct. and Anal. of Syst., pages 530–545.

    Google Scholar 

  53. Zhu, J. and Calman, S. (2004). Symbolic pointer analysis revisited. In Prog. Lang. Design and Impl.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Tel Aviv University, Tel Aviv, 69978, Israel

    Mooly Sagiv

  2. Computer Sciences Department, University of Wisconsin, 1210 W. Dayton St., Madison, WI, 53706, USA

    Thomas W. Reps

  3. Fachrichtung Informatik, Universitat des Saarlandes, 66123, Saarbrücken

    Reinhard Wilhelm

  4. IBM T.J. Watson Research Center, Yorktown Heights, NY, 10598, USA

    Eran Yahav

Authors
  1. Mooly Sagiv
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas W. Reps
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Reinhard Wilhelm
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Eran Yahav
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technische Universität München, Garching, Germany

    Manfred Broy  & Johannes Grünbauer  & 

  2. The Weizmann Institute of Science, Rehovot, Israel

    David Harel

  3. Microsoft Research, Cambridge, UK

    Tony Hoare

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer

About this paper

Cite this paper

Sagiv, M., Reps, T.W., Wilhelm, R., Yahav, E. (2005). On the Utility of Canonical Abstraction. In: Broy, M., Grünbauer, J., Harel, D., Hoare, T. (eds) Engineering Theories of Software Intensive Systems. NATO Science Series, vol 195. Springer, Dordrecht. https://doi.org/10.1007/1-4020-3532-2_8

Download citation

  • DOI: https://doi.org/10.1007/1-4020-3532-2_8

  • Publisher Name: Springer, Dordrecht

  • Print ISBN: 978-1-4020-3530-2

  • Online ISBN: 978-1-4020-3532-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation