Reachability Analysis of Pushdown Systems with an Upper Stack

  • Adrien PommelletEmail author
  • Marcio Diaz
  • Tayssir Touili
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10168)


Pushdown systems (PDSs) are a natural model for sequential programs, but they can fail to accurately represent the way an assembly stack actually operates. Indeed, one may want to access the part of the memory that is below the current stack or base pointer, hence the need for a model that keeps track of this part of the memory. To this end, we introduce pushdown systems with an upper stack (UPDSs), an extension of PDSs where symbols popped from the stack are not destroyed but instead remain just above its top, and may be overwritten by later push rules. We prove that the sets of successors \(post^*\) and predecessors \(pre^*\) of a regular set of configurations of such a system are not always regular, but that \(post^*\) is context-sensitive, so that we can decide whether a single configuration is forward reachable or not. In order to underapproximate \(pre^*\) in a regular fashion, we consider a bounded-phase analysis of UPDSs, where a phase is a part of a run during which either push or pop rules are forbidden. We then present a method to overapproximate \(post^*\) that relies on regular abstractions of runs of UPDSs. Finally, we show how these approximations can be used to detect stack overflows and stack pointer manipulations with malicious intent.


Pushdown systems Reachability analysis Stack pointer Finite automata 


  1. 1.
    Bermudez, M.E., Schimpf, K.M.: Practical arbitrary lookahead LR parsing. J. Comput. Syst. Sci. 41, 230–250 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997). doi: 10.1007/3-540-63141-0_10 Google Scholar
  3. 3.
    Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL 2003 (2003)Google Scholar
  4. 4.
    Carotenuto, D., Murano, A., Peron, A.: 2-visibly pushdown automata. In: Harju, T., Karhumäki, J., Lepistö, A. (eds.) DLT 2007. LNCS, vol. 4588, pp. 132–144. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-73208-2_15 CrossRefGoogle Scholar
  5. 5.
    Caucal, D.: On the regular structure of prefix rewriting. Theor. Comput. Sci. 106, 61–86 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000). doi: 10.1007/10722167_20 CrossRefGoogle Scholar
  7. 7.
    Ginsburg, S., Greibach, S.A., Harrison, M.A.: Stack automata and compiling. J. ACM 14, 172–201 (1967)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Hopcroft, J., Ullman, J.: Sets accepted by one-way stack automata are context sensitive. Inf. Control 13, 114–133 (1968)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Pereira, F.C.N., Wright, R.N.: Finite-state approximation of phrase structure grammars. In: ACL 1991 (1991)Google Scholar
  10. 10.
    Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005). doi: 10.1007/978-3-540-31980-1_7 CrossRefGoogle Scholar
  11. 11.
    Seth, A.: Global reachability in bounded phase multi-stack pushdown systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 615–628. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-14295-6_53 CrossRefGoogle Scholar
  12. 12.
    Torre, S.L., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS 2007 (2007)Google Scholar
  13. 13.
    Uezato, Y., Minamide, Y.: Pushdown systems with stack manipulation. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 412–426. Springer, Heidelberg (2013). doi: 10.1007/978-3-319-02444-8_29 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.LIPNUniversité Paris-DiderotParisFrance
  2. 2.LIPN, CNRSUniversité Paris 13VilletaneuseFrance

Personalised recommendations