{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:30:06Z","timestamp":1767929406678,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642333859","type":"print"},{"value":"9783642333866","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33386-6_13","type":"book-chapter","created":{"date-parts":[[2012,9,28]],"date-time":"2012-09-28T10:58:20Z","timestamp":1348829900000},"page":"152-166","source":"Crossref","is-referenced-by-count":13,"title":["Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding"],"prefix":"10.1007","author":[{"given":"Mohamed Faouzi","family":"Atig","sequence":"first","affiliation":[]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[]},{"given":"K.","family":"Narayan Kumar","sequence":"additional","affiliation":[]},{"given":"Prakash","family":"Saivasan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-24730-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2004","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A Temporal Logic of Nested Calls and Returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 467\u2013481. Springer, Heidelberg (2004)"},{"key":"13_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":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-00768-2_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.F. Atig","year":"2009","unstructured":"Atig, M.F., Bouajjani, A., Qadeer, S.: Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 107\u2013123. Springer, Heidelberg (2009)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-15375-4_9","volume-title":"CONCUR 2010 - Concurrency Theory","author":"M.F. Atig","year":"2010","unstructured":"Atig, M.F.: From Multi to Single Stack Automata. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 117\u2013131. Springer, Heidelberg (2010)"},{"key":"13_CR5","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":"13_CR6","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":"13_CR7","unstructured":"Atig, M.F., Bouajjani, A., Narayan Kumar, K., Saivasan, P.: Model checking branching-time properties of multi-pushdown systems is hard. CoRR abs\/1205.6928 (2012)"},{"key":"13_CR8","unstructured":"Atig, M.F., Bouajjani, A., Touili, T.: Analyzing asynchronous programs with preemption. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008). LIPIcs, vol.\u00a02, pp. 37\u201348. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2008)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-540-85361-9_29","volume-title":"CONCUR 2008 - Concurrency Theory","author":"M.F. Atig","year":"2008","unstructured":"Atig, M.F., Bouajjani, A., Touili, T.: On the Reachability Analysis of Acyclic Networks of Pushdown Systems. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol.\u00a05201, pp. 356\u2013371. Springer, Heidelberg (2008)"},{"key":"13_CR10","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\u201997: 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.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Maler, O.: Reachability analysis of pushdown automata. In: Proc. Intern. Workshop on Verification of Infinite-State Systems, Infinity 1996 (1996)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/11539452_36","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., M\u00fcller-Olm, M., Touili, T.: Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 473\u2013487. Springer, Heidelberg (2005)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-23702-7_13","volume-title":"Static Analysis","author":"A. Bouajjani","year":"2011","unstructured":"Bouajjani, A., Emmi, M., Parlato, G.: On Sequentializing Concurrent Programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 129\u2013145. Springer, Heidelberg (2011)"},{"key":"13_CR14","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: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 348\u2013359. Springer, Heidelberg (2005)"},{"key":"13_CR15","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":"13_CR16","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. Intl. Journal of Foundations of Computer Science\u00a07(3), 253\u2013292 (1996)","journal-title":"Intl. Journal of Foundations of Computer Science"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Emmi, M., Qadeer, S., Rakamari\u0107, Z.: Delay-bounded scheduling. In: POPL 2011: Proc. 38th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 411\u2013422. ACM (2011)","DOI":"10.1145\/1926385.1926432"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-642-14295-6_52","volume-title":"Computer Aided Verification","author":"P. Ganty","year":"2010","unstructured":"Ganty, P., Majumdar, R., Monmege, B.: Bounded Underapproximations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 600\u2013614. Springer, Heidelberg (2010)"},{"key":"13_CR19","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979)"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: Proceedings of LICS, pp. 161\u2013170. IEEE (2007)","DOI":"10.1109\/LICS.2007.9"},{"key":"13_CR21","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. La Torre","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":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/978-3-642-14295-6_54","volume-title":"Computer Aided Verification","author":"S. La Torre","year":"2010","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Model-Checking Parameterized Concurrent Programs Using Linear Interfaces. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 629\u2013644. Springer, Heidelberg (2010)"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2009), pp. 211\u2013222. ACM (2009)","DOI":"10.1145\/1542476.1542500"},{"key":"13_CR24","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. La Torre","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":"13_CR25","unstructured":"La Torre, S., Napoli, M.: A temporal logic for multi-threaded programs. In: IFIP TCS. IFIP. Springer (to appear, 2012)"},{"key":"13_CR26","unstructured":"La Torre, S., Parlato, G.: Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width. Technical report, University of Southampton (March 2012)"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-70545-1_7","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2008","unstructured":"Lal, A., Reps, T.: Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 37\u201351. Springer, Heidelberg (2008)"},{"key":"13_CR28","unstructured":"Lange, M., Lei\u00df, H.: To CNF or not to CNF ? An efficient yet presentable version of the CYK algorithm. Informatica Didactica 8 (2008-2010)"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI, pp. 446\u2013455. ACM (2007)","DOI":"10.1145\/1273442.1250785"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"13_CR31","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)"},{"issue":"2","key":"13_CR32","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst.\u00a022(2), 416\u2013430 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/11817963_29","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2006","unstructured":"Sen, K., Viswanathan, M.: Model Checking Multithreaded Programs with Asynchronous Atomic Methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 300\u2013314. Springer, Heidelberg (2006)"},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: POPL, pp. 250\u2013259 (1988)","DOI":"10.1145\/73560.73582"},{"key":"13_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/BFb0015261","volume-title":"Computer Science Today","author":"M.Y. Vardi","year":"1995","unstructured":"Vardi, M.Y.: Alternating Automata and Program Verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 471\u2013485. Springer, Heidelberg (1995)"},{"key":"13_CR36","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)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33386-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T18:10:18Z","timestamp":1744222218000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33386-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642333859","9783642333866"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33386-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}