{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:16:09Z","timestamp":1770977769369,"version":"3.50.1"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319537320","type":"print"},{"value":"9783319537337","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-53733-7_33","type":"book-chapter","created":{"date-parts":[[2017,2,15]],"date-time":"2017-02-15T05:39:21Z","timestamp":1487137161000},"page":"447-459","source":"Crossref","is-referenced-by-count":1,"title":["Reachability Analysis of Pushdown Systems with an Upper Stack"],"prefix":"10.1007","author":[{"given":"Adrien","family":"Pommellet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcio","family":"Diaz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,16]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1016\/0022-0000(90)90037-L","volume":"41","author":"ME Bermudez","year":"1990","unstructured":"Bermudez, M.E., Schimpf, K.M.: Practical arbitrary lookahead LR parsing. J. Comput. Syst. Sci. 41, 230\u2013250 (1990)","journal-title":"J. Comput. Syst. Sci."},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR 1997: Concurrency Theory","author":"A Bouajjani","year":"1997","unstructured":"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\u2013150. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63141-0_10"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL 2003 (2003)","DOI":"10.1145\/604131.604137"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-540-73208-2_15","volume-title":"Developments in Language Theory","author":"D Carotenuto","year":"2007","unstructured":"Carotenuto, D., Murano, A., Peron, A.: 2-visibly pushdown automata. In: Harju, T., Karhum\u00e4ki, J., Lepist\u00f6, A. (eds.) DLT 2007. LNCS, vol. 4588, pp. 132\u2013144. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73208-2_15"},{"key":"33_CR5","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0304-3975(92)90278-N","volume":"106","author":"D Caucal","year":"1992","unstructured":"Caucal, D.: On the regular structure of prefix rewriting. Theor. Comput. Sci. 106, 61\u201386 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2000","unstructured":"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\u2013247. Springer, Heidelberg (2000). doi: 10.1007\/10722167_20"},{"key":"33_CR7","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1145\/321371.321385","volume":"14","author":"S Ginsburg","year":"1967","unstructured":"Ginsburg, S., Greibach, S.A., Harrison, M.A.: Stack automata and compiling. J. ACM 14, 172\u2013201 (1967)","journal-title":"J. ACM"},{"key":"33_CR8","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1016\/S0019-9958(68)90722-5","volume":"13","author":"J Hopcroft","year":"1968","unstructured":"Hopcroft, J., Ullman, J.: Sets accepted by one-way stack automata are context sensitive. Inf. Control 13, 114\u2013133 (1968)","journal-title":"Inf. Control"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Pereira, F.C.N., Wright, R.N.: Finite-state approximation of phrase structure grammars. In: ACL 1991 (1991)","DOI":"10.3115\/981344.981376"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Qadeer","year":"2005","unstructured":"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\u2013107. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-31980-1_7"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1007\/978-3-642-14295-6_53","volume-title":"Computer Aided Verification","author":"A Seth","year":"2010","unstructured":"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\u2013628. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14295-6_53"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Torre, S.L., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS 2007 (2007)","DOI":"10.1109\/LICS.2007.9"},{"key":"33_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-319-02444-8_29","volume-title":"Automated Technology for Verification and Analysis","author":"Y Uezato","year":"2013","unstructured":"Uezato, Y., Minamide, Y.: Pushdown systems with stack manipulation. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 412\u2013426. Springer, Heidelberg (2013). doi: 10.1007\/978-3-319-02444-8_29"}],"container-title":["Lecture Notes in Computer Science","Language and Automata Theory and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-53733-7_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T06:35:56Z","timestamp":1498372556000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-53733-7_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319537320","9783319537337"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-53733-7_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}