Skip to main content
SpringerLink
Log in

Context-Sensitive Relevancy Analysis for Efficient Symbolic Execution

  • Conference paper
Programming Languages and Systems (APLAS 2008)

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

Included in the following conference series:

Abstract

Symbolic execution is a flexible and powerful, but computationally expensive technique to detect dynamic behaviors of a program. In this paper, we present a context-sensitive relevancy analysis algorithm based on weighted pushdown model checking, which pinpoints memory locations in the program where symbolic values can flow into. This information is then utilized by a code instrumenter to transform only relevant parts of the program with symbolic constructs, to help improve the efficiency of symbolic execution of Java programs. Our technique is evaluated on a generalized symbolic execution engine that is developed upon Java Path Finder with checking safety properties of Java applications. Our experiments indicate that this technique can effectively improve the performance of the symbolic execution engine with respect to the approach that blindly instruments the whole program.

D.Shannon was an intern at Fujistu Labs. Sunnyvale during this work.

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. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  2. Deng, X., Lee, J., Robby: Bogor/Kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In: The 21st IEEE International Conference on Automated Software Engineering (ASE 2006), pp. 157–166 (2006)

    Google Scholar 

  3. Khurshid, S., Pasareanu, C., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Anand, S., Pasareanu, C.S., Visser, W.: JPF-SE: A symbolic execution extension to Java PathFinder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 134–138. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Reps, T.W., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. 58(1-2), 206–263 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  6. Hunt, S.: PERs generalize projections for strictness analysis. In: Functional Programming. Proc. 1990 Glasgow Workshop, pp. 114–125. Springer, Heidelberg (1990)

    Google Scholar 

  7. Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: The 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 1998), pp. 38–48 (1998)

    Google Scholar 

  8. Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L.J., Lam, P., Sundaresan, V.: Soot - a Java bytecode optimization framework. In: Conference of the Centre for Advanced Studies on Collaborative Research, CASCON 1999 (1999)

    Google Scholar 

  9. Hasti, R., Horwitz, S.: Using static single assignment form to improve flow-insensitive pointer analysis. In: ACM SIGPLAN conference on Programming language design and implementation (PLDI 1998), pp. 97–105 (1998)

    Google Scholar 

  10. Li, X., Ogawa, M.: Interprocedural program analysis for java based on weighted pushdown model checking. In: The 5th International Workshop on Automated Verification of Infinite-State Systems (AVIS 2006), ETAPS (April 2006)

    Google Scholar 

  11. Reps, T.W.: Program analysis via graph reachability. In: International Logic Programming Symposium (ILPS 1997), pp. 5–19. MIT Press, Cambridge (1997)

    Google Scholar 

  12. Reps, T.W., Lal, A., Kidd, N.: Program analysis using weighted pushdown systems. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 23–51. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  13. Shivers, O.: Control flow analysis in scheme. In: ACM SIGPLAN conference on Programming Language design and Implementation (PLDI 1988), pp. 164–174 (1988)

    Google Scholar 

  14. Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2004), pp. 131–144 (2004)

    Google Scholar 

  15. Tkachuk, O., Dwyer, M.B., Păsăreanu, C.: Automated environment generation for software model checking. In: The 18th IEEE International Conference on Automated Software Engineering (ASE 2003), pp. 116–129 (2003)

    Google Scholar 

  16. Khurshid, S., Suen, Y.L.: Generalizing symbolic execution to library classes. In: ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering (PASTE 2005), pp. 103–110 (2005)

    Google Scholar 

  17. Dwyer, M., Hatcliff, J., Joehanes, R., Laubach, S., Pasareanu, C.S., Robby, Zheng, H., Visser, W.: Tool-supported program abstraction for finite-state verification. In: The 23rd International Conference on Software Engineering (ICSE 2001), pp. 177–187 (2001)

    Google Scholar 

  18. Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically generating inputs of death. In: ACM Conference on Computer and Communications Security 2006 (CCS 2006), pp. 322–335 (2006)

    Google Scholar 

  19. Schulte, W., Grieskamp, W., Tillmann, N.: XRT-exploring runtime for.NET architecture and applications. Electronic Notes in Theoretical Computer Science 144(3), 3–26 (2006)

    Article  Google Scholar 

  20. Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: ESEC/FSE-13: Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, pp. 263–272. ACM, New York (2005)

    Chapter  Google Scholar 

  21. Anand, S., Orso, A., Harrold, M.J.: Type-dependence analysis and program transformation for symbolic execution. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 117–133. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  22. Livshits, V.B., Lam, M.S.: Finding security vulnerabilities in Java applications with static analysis. In: The 14th conference on USENIX Security Symposium (SSYM 2005), p. 18. USENIX Association (2005)

    Google Scholar 

  23. Christensen, A., Møller, A., Schwartzbach, M.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1–18. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Science, Japan Advanced Institute of Science and Technology, Nomi, Japan

    Xin Li & Mizuhito Ogawa

  2. Department of Electrical and Computer Engineering, University of Texas at Austin, Austin, TX, USA

    Daryl Shannon & Sarfraz Khurshid

  3. Trusted Systems Innovation Group, Fujitsu laboratory of America, Sunnyvale, CA, USA

    Indradeep Ghosh & Sreeranga P. Rajan

Authors
  1. Xin Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Daryl Shannon
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Indradeep Ghosh
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mizuhito Ogawa
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Sreeranga P. Rajan
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Sarfraz Khurshid
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research India, 196/36, 2nd Main, Sadashivnagar, 560080, Bangalore, India

    G. Ramalingam

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Li, X., Shannon, D., Ghosh, I., Ogawa, M., Rajan, S.P., Khurshid, S. (2008). Context-Sensitive Relevancy Analysis for Efficient Symbolic Execution. In: Ramalingam, G. (eds) Programming Languages and Systems. APLAS 2008. Lecture Notes in Computer Science, vol 5356. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89330-1_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-89330-1_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-89329-5

  • Online ISBN: 978-3-540-89330-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation