Skip to main content
SpringerLink
Log in

State Space Exploration

  • Chapter
  • First Online:
Book cover String Analysis for Software Verification and Security

  • 671 Accesses

Abstract

In this chapter we provide a basic survey of reachability analysis for verification of string manipulating programs starting with explicit state enumeration. We discuss both forward and backward reachability analysis using depth-first search where states of a given string manipulating program are traversed one state at a time. Next, we discuss symbolic reachability analysis, where the basic idea is to perform state exploration using sets of states rather than traversing states one by one. We discuss that reachability analysis corresponds to fixpoint computations, and, in order to develop a symbolic analysis framework for string manipulating programs, we need to first develop a symbolic representation that can represent sets of strings.

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

Access this chapter

Log in via an institution

Institutional subscriptions

References

  1. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.

    Article  MathSciNet  MATH  Google Scholar 

  2. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 2001. http://books.google.de/books?id=Nmc4wEaLXFEC

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of California, Santa Barbara, Santa Barbara, CA, USA

    Tevfik Bultan

  2. Department of Management, Information Systems, National Chenchi University, Taipei, Taiwan

    Fang Yu

  3. Computer Science Department, King Saud University, Riyadh, Saudi Arabia

    Muath Alkhalaf

  4. Microsoft (United States), Redmond, WA, USA

    Abdulbaki Aydin

Authors
  1. Tevfik Bultan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fang Yu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Muath Alkhalaf
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Abdulbaki Aydin
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bultan, T., Yu, F., Alkhalaf, M., Aydin, A. (2017). State Space Exploration. In: String Analysis for Software Verification and Security. Springer, Cham. https://doi.org/10.1007/978-3-319-68670-7_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68670-7_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68668-4

  • Online ISBN: 978-3-319-68670-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation