{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T17:36:11Z","timestamp":1725730571385},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642387708"},{"type":"electronic","value":"9783642387715"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38771-5_7","type":"book-chapter","created":{"date-parts":[[2013,6,9]],"date-time":"2013-06-09T22:16:25Z","timestamp":1370816185000},"page":"58-69","source":"Crossref","is-referenced-by-count":4,"title":["Adjacent Ordered Multi-Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Mohamed Faouzi","family":"Atig","sequence":"first","affiliation":[]},{"given":"K.","family":"Narayan Kumar","sequence":"additional","affiliation":[]},{"given":"Prakash","family":"Saivasan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"Atig, M.F.: Global model checking of ordered multi-pushdown systems. In: FSTTCS. LIPIcs, vol.\u00a08, pp. 216\u2013227. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)","key":"7_CR1"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-85780-8_9","volume-title":"Developments in Language Theory","author":"M.F. Atig","year":"2008","unstructured":"Atig, M.F., Bollig, B., Habermehl, P.: Emptiness of multi-pushdown automata is 2ETIME-complete. In: Ito, M., Toyama, M. (eds.) DLT 2008. LNCS, vol.\u00a05257, pp. 121\u2013133. Springer, Heidelberg (2008)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-31424-7_19","volume-title":"Computer Aided Verification","author":"M.F. Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Emmi, M., Lal, A.: Detecting fair non-termination in multithreaded programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 210\u2013226. Springer, Heidelberg (2012)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-33386-6_13","volume-title":"Automated Technology for Verification and Analysis","author":"M.F. Atig","year":"2012","unstructured":"Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Linear-time model-checking for multithreaded programs under scope-bounding. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 152\u2013166. Springer, Heidelberg (2012)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-22993-0_15","volume-title":"Mathematical Foundations of Computer Science 2011","author":"B. Bollig","year":"2011","unstructured":"Bollig, B., Cyriac, A., Gastin, P., Zeitoun, M.: Temporal logics for concurrent recursive programs: Satisfiability and model checking. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol.\u00a06907, pp. 132\u2013144. Springer, Heidelberg (2011)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11590156_28","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Esparza, J., Schwoon, S., Strej\u010dek, J.: Reachability analysis of multithreaded software with asynchronous communication. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 348\u2013359. Springer, Heidelberg (2005)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-73368-3_24","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2007","unstructured":"Bouajjani, A., Fratani, S., Qadeer, S.: Context-bounded analysis of multithreaded programs with dynamic linked structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 207\u2013220. Springer, Heidelberg (2007)"},{"issue":"3","key":"7_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1142\/S0129054196000191","volume":"7","author":"L. Breveglieri","year":"1996","unstructured":"Breveglieri, L., Cherubini, A., Citrini, C., Crespi-Reghizzi, S.: Multi-push-down languages and grammars. Int. J. Found. Comput. Sci.\u00a07(3), 253\u2013292 (1996)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-32940-1_38","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"A. Cyriac","year":"2012","unstructured":"Cyriac, A., Gastin, P., Kumar, K.N.: MSO decidability of multi-pushdown systems via split-width. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 547\u2013561. Springer, Heidelberg (2012)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-12032-9_19","volume-title":"Foundations of Software Science and Computational Structures","author":"A. Heu\u00dfner","year":"2010","unstructured":"Heu\u00dfner, A., Leroux, J., Muscholl, A., Sutre, G.: Reachability analysis of communicating pushdown systems. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol.\u00a06014, pp. 267\u2013281. Springer, Heidelberg (2010)"},{"issue":"1","key":"7_CR11","first-page":"73","volume":"35","author":"A. Lal","year":"2009","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. FMSD\u00a035(1), 73\u201397 (2009)","journal-title":"FMSD"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-540-78800-3_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Lal","year":"2008","unstructured":"Lal, A., Touili, T., Kidd, N., Reps, T.W.: Interprocedural analysis of concurrent programs under a context bound. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 282\u2013298. Springer, Heidelberg (2008)"},{"doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: POPL, pp. 283\u2013294. ACM (2011)","key":"7_CR13","DOI":"10.1145\/1925844.1926419"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","key":"7_CR14","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR15","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.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"7_CR16","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.\u00a06174, pp. 615\u2013628. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS, pp. 161\u2013170. IEEE Computer Society (2007)","key":"7_CR17","DOI":"10.1109\/LICS.2007.9"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-78800-3_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Torre La","year":"2008","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Context-bounded analysis of concurrent queue systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 299\u2013314. Springer, Heidelberg (2008)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-87531-4_5","volume-title":"Computer Science Logic","author":"S. Torre La","year":"2008","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: An infinite automaton characterization of double exponential time. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 33\u201348. Springer, Heidelberg (2008)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-02658-4_36","volume-title":"Computer Aided Verification","author":"S. Torre La","year":"2009","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 477\u2013492. Springer, Heidelberg (2009)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-23217-6_14","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"S. Torre La","year":"2011","unstructured":"La Torre, S., Napoli, M.: Reachability of multistack pushdown systems with scope-bounded matching relations. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 203\u2013218. Springer, Heidelberg (2011)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-33475-7_16","volume-title":"Theoretical Computer Science","author":"S. Torre La","year":"2012","unstructured":"La Torre, S., Napoli, M.: A temporal logic for multi-threaded programs. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol.\u00a07604, pp. 225\u2013239. Springer, Heidelberg (2012)"},{"doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: POPL, pp. 250\u2013259 (1988)","key":"7_CR23","DOI":"10.1145\/73560.73582"},{"unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp. 332\u2013344. IEEE Computer Society (1986)","key":"7_CR24"}],"container-title":["Lecture Notes in Computer Science","Developments in Language Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38771-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T20:27:02Z","timestamp":1557779222000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38771-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642387708","9783642387715"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38771-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}