Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Symbolic execution with abstraction

  • SPECIAL SECTION ON SPIN
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

We address the problem of error detection for programs that take recursive data structures and arrays as input. Previously we proposed a combination of symbolic execution and model checking for the analysis of such programs: we put a bound on the size of the program inputs and/or the search depth of the model checker to limit the search state space. Here we look beyond bounded model checking and consider state matching techniques to limit the state space. We describe a method for examining whether a symbolic state that arises during symbolic execution is subsumed by another symbolic state. Since the number of symbolic states may be infinite, subsumption is not enough to ensure termination. Therefore, we also consider abstraction techniques for computing and storing abstract states during symbolic execution. Subsumption checking determines whether an abstract state is being revisited, in which case the model checker backtracks—this enables analysis of an under-approximation of the program behaviors. We illustrate the technique with abstractions for lists and arrays. We also discuss abstractions for more general data structures. The abstractions encode both the shape of the program heap and the constraints on numeric data. We have implemented the techniques in the Java PathFinder tool and we show their effectiveness on Java programs. This paper is an extended version of Anand et al. (Proceedings of SPIN, pp. 163–181, 2006).

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Anand, S., Orso, A., Harrold, M.J.: Type-dependence analysis and program transformation for symbolic execution. In: Proceedings of TACAS, pp. 117–133 (2007)

  2. Anand, S., Pasareanu, C.S., Visser, W.: Symbolic execution with abstract subsumption checking. In: Proceedings of SPIN, pp. 163–181 (2006)

  3. Anand, S., Pasareanu, C.S., Visser, W.: JPF-SE: a symbolic execution extension to Java Pathfinder. In: Proceedings of TACAS, pp. 134–138 (2007)

  4. Ball, T.: A theory of predicate-complete test coverage and generation. MSR-TR-2004-28 (2004)

  5. Ball, T., Kupferman, O., Yorsh, G.: Abstraction for falsification. In: Proceedings of CAV, pp. 67–81 (2005)

  6. Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Proceedings of CAV, pp. 260–264 (2001)

  7. Chaki S., Clarke E., Groce A., Jha S., Veith H.: Modular verification of software components in C. ACM Trans. Comput. Syst. 30(6), 388–402 (2004)

    Google Scholar 

  8. Dams, D., Namjoshi, K.S.: Shape analysis through predicate abstraction and model checking. In: Proceedings of VMCAI, pp. 310–324 (2003)

  9. Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings of POPL, pp. 191–202 (2002)

  10. Flyod, R.W.: Assigning meanings to programs. In: Proceedings of symposia in applied mathematics, vol. 19, pp. 19–32 (1967)

  11. Ghiya, R., Hendren, L.J.: Is it a tree, a DAG, or a cyclic graph? a shape analysis for heap-directed pointers in c. In: Proceedings of POPL, pp. 1–15 (1996)

  12. Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: Proceedings of PLDI, pp. 213–223 (2005)

  13. Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Proceedings of TACAS, pp. 512–529 (2004)

  14. Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: Proceedings of POPL, pp. 338–350 (2005)

  15. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Proceedings of SPIN, pp. 235–239 (2003)

  16. Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Proceedings of SPIN, pp. 76–91 (2004)

  17. Java PathFinder. http://javapathfinder.sourceforge.net

  18. Khurshid, S., Păsăreanu, C., Visser, W.: Generalized symbolic execution for model checking and testing. In: Proceedings of TACAS, pp. 553–568 (2003)

  19. Khurshid, S., Suen, Y.: Generalizing symbolic execution to library classes. In: Proceedings of PASTE, pp. 103–110 (2005)

  20. King J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MATH  Google Scholar 

  21. Kuncak, V., Rinard, M.: Existential heap abstraction entailment is undecidable. In: Proceedings of SAS, pp. 418–438 (2003)

  22. Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Proceedings of VMCAI, pp. 181–198 (2005)

  23. Păsăreanu, C., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Proceedings of SPIN, pp. 164–181 (2004)

  24. Păsăreanu C.S., Dwyer M.B., Visser W.: Finding feasible abstract counter-examples. STTT 5(1), 34–48 (2003)

    Google Scholar 

  25. Păsăreanu, C.S., Pelánek, R., Visser, W.: Concrete model checking with abstract matching and refinement. In: Proceedings of CAV, pp. 52–66 (2005)

  26. Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. Commun. ACM, 31(8), August (1992)

  27. Sagiv S., Reps T.W., Wilhelm R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002)

    Article  Google Scholar 

  28. Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of ESEC/SIGSOFT FSE, pp. 263–272 (2005)

  29. Visser W., Havelund K., Brat G., Park S.J., Lerda F.: Model checking programs. Autom Softw Eng J 10(2), 203–232 (2003)

    Article  Google Scholar 

  30. Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: a framework for generating object-oriented unit tests using symbolic execution. In: Proceedings of TACAS, pp. 365–381 (2005)

  31. Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Proceedings of SAS, pp. 69–84 (2002)

Download references

Author information

Authors and Affiliations

  1. College of Computing, Georgia Institute of Technology, Atlanta, GA, USA

    Saswat Anand

  2. NASA Ames Research Center, Moffett Field, Mountain View, CA, 94035, USA

    Corina S. Păsăreanu

  3. SEVEN Networks, Redwood City, CA, USA

    Willem Visser

Authors
  1. Saswat Anand
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Corina S. Păsăreanu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Willem Visser
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Saswat Anand.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Anand, S., Păsăreanu, C.S. & Visser, W. Symbolic execution with abstraction. Int J Softw Tools Technol Transfer 11, 53–67 (2009). https://doi.org/10.1007/s10009-008-0090-1

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-008-0090-1

Keywords

Search

Navigation