{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,15]],"date-time":"2026-05-15T12:25:36Z","timestamp":1778847936490,"version":"3.51.4"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,5,4]],"date-time":"2013-05-04T00:00:00Z","timestamp":1367625600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10009-013-0276-z","type":"journal-article","created":{"date-parts":[[2013,5,3]],"date-time":"2013-05-03T04:16:15Z","timestamp":1367554575000},"page":"127-146","source":"Crossref","is-referenced-by-count":9,"title":["Bounded phase analysis of message-passing programs"],"prefix":"10.1007","volume":"16","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[]},{"given":"Michael","family":"Emmi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,5,4]]},"reference":[{"key":"276_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: LICS \u201993: Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science, pp. 160\u2013170. IEEE Computer Society (1993)","DOI":"10.1109\/LICS.1993.287591"},{"key":"276_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy fifo channels. In: CAV \u201998: Proceedings of the 10th International Conference on Computer Aided Verification, vol. 1427 of LNCS, pp. 305\u2013318. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028754"},{"key":"276_CR3","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bollig, B., Habermehl, P.: Emptiness of multi-pushdown automata is 2etime-complete. In: DLT \u201908: Proceedings of the 12th International Conference on Developments in Language Theory, vol. 5257 of LNCS, pp. 121\u2013133. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-85780-8_9"},{"key":"276_CR4","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Emmi, M., Lal, A.: Detecting fair non-termination in multithreaded programs. In: CAV \u201912: Proceedings of the 24th International Conference on Computer Aided Verification, vol. 7358 of LNCS. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-31424-7_19"},{"key":"276_CR5","unstructured":"Barnett, M., Leino, K.R.M. Moskal, M., Schulte W.: Boogie: an intermediate verification language. http:\/\/research.microsoft.com\/en-us\/projects\/boogie\/ . Accessed 1 Jan 2012"},{"issue":"3","key":"276_CR6","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1008719024240","volume":"14","author":"B Boigelot","year":"1999","unstructured":"Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. Form. Methods Syst. Design 14(3), 237\u2013255 (1999)","journal-title":"Form. Methods Syst. Design"},{"key":"276_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. In: TACAS \u201912: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 7214 of LNCS, pp. 451\u2013465. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28756-5_31"},{"issue":"1\u20132","key":"276_CR8","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/S0304-3975(99)00033-X","volume":"221","author":"A Bouajjani","year":"1999","unstructured":"Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of fifo-channel systems with nonregular sets of configurations. Theor. Comput. Sci. 221(1\u20132), 211\u2013250 (1999)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"276_CR9","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/s10703-008-0048-7","volume":"32","author":"A Bouajjani","year":"2008","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Verification of parametric concurrent systems with prioritised FIFO resource management. Form. Methods Syst. Design 32(2), 129\u2013172 (2008)","journal-title":"Form. Methods Syst. Design"},{"key":"276_CR10","doi-asserted-by":"crossref","unstructured":"Bouajjani, A. Emmi, M., Parlato G.: On sequentializing concurrent programs. In: SAS \u201911: Proceedings of the 18th International Symposium on Static Analysis, vol. 6887 of LNCS, pp. 129\u2013145. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-23702-7_13"},{"issue":"2","key":"276_CR11","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"key":"276_CR12","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S.: Subcubic algorithms for recursive state machines. In: POPL \u201908: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 159\u2013169. ACM, New York (2008)","DOI":"10.1145\/1328438.1328460"},{"key":"276_CR13","unstructured":"Dahl, R.: Node.js: Evented I\/O for V8 JavaScript. http:\/\/nodejs.org\/ . Accessed 1 Jan 2012"},{"key":"276_CR14","doi-asserted-by":"crossref","unstructured":"Emmi, M., Lal, A.: Finding non-terminating executions in distributed asynchronous programs. In: SAS \u201912: Proceedings of the 19th International Static Analysis Symposium, LNCS, pp. 439\u2013455. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-33125-1_29"},{"key":"276_CR15","doi-asserted-by":"crossref","unstructured":"Emmi, M. Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: POPL \u201911: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 411\u2013422. ACM, New York (2011)","DOI":"10.1145\/1926385.1926432"},{"key":"276_CR16","doi-asserted-by":"crossref","unstructured":"Emmi, M., Lal, A., Qadeer, S.: Asynchronous programs with prioritized task-buffers. In: FSE \u201912: Proceedings of the 20th International Symposium on the Foundations of Software Engineering. ACM, New York (2012)","DOI":"10.1145\/2393596.2393652"},{"issue":"2","key":"276_CR17","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1016\/S0890-5401(03)00139-1","volume":"186","author":"J Esparza","year":"2003","unstructured":"Esparza, J., Kucera, A., Schwoon, S.: Model checking ltl with regular valuations for pushdown systems. Inf. Comput. 186(2), 355\u2013376 (2003)","journal-title":"Inf. Comput."},{"key":"276_CR18","doi-asserted-by":"crossref","unstructured":"Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst. 34(1), 6 (2012)","DOI":"10.1145\/2160910.2160915"},{"key":"276_CR19","doi-asserted-by":"crossref","unstructured":"Ganty, P., Majumdar, R., Rybalchenko, A.: Verifying liveness for asynchronous programs. In: POPL 09: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 102\u2013113. ACM, New York (2009)","DOI":"10.1145\/1480881.1480895"},{"issue":"2\u20133","key":"276_CR20","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1016\/j.tcs.2008.09.019","volume":"410","author":"P Haller","year":"2009","unstructured":"Haller, P., Odersky, M.: Scala actors: unifying thread-based and event-based programming. Theor. Comput. Sci. 410(2\u20133), 202\u2013220 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"276_CR21","doi-asserted-by":"crossref","unstructured":"Heu\u00dfner, A., Leroux, J., Muscholl, A., Sutre, G.: Reachability analysis of communicating pushdown systems. In: FOSSACS \u201910: Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures, vol. 6014 of LNCS, pp. 267\u2013281. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-12032-9_19"},{"key":"276_CR22","unstructured":"HTML5: A vocabulary and associated APIs for HTML and XHTML. http:\/\/dev.w3.org\/html5\/spec\/Overview.html . Accessed 1 Jan 2012"},{"key":"276_CR23","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL \u201907: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 339\u2013350. ACM, New York (2007)","DOI":"10.1145\/1190216.1190266"},{"key":"276_CR24","doi-asserted-by":"crossref","unstructured":"Kidd, N., Jagannathan, S., Vitek, J.: One stack to run them all: reducing concurrent analysis to sequential analysis under priority scheduling. In: SPIN \u201910: Proceedings of the 17th International Workshop on Model Checking Software, vol. 6349 of LNCS, pp. 245\u2013261. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-16164-3_18"},{"key":"276_CR25","unstructured":"La Torre S., Parlato, G.: Scope-bounded multistack pushdown systems: fixed-point, sequentialization, and tree-width. In: FSTTCS \u201912: Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 18 of LIPIcs, pp. 173\u2013184. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2012)"},{"key":"276_CR26","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS \u201907: Proceedings of the 22nd IEEE Symposium on Logic in Computer Science, pp. 161\u2013170. IEEE Computer Society (2007)","DOI":"10.1109\/LICS.2007.9"},{"key":"276_CR27","doi-asserted-by":"crossref","unstructured":"La Torre, S. Madhusudan, P., Parlato G.: Context-bounded analysis of concurrent queue systems. In: TACAS \u201908: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 4963 of LNCS, pp. 299\u2013314. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_21"},{"key":"276_CR28","doi-asserted-by":"crossref","unstructured":"La Torre, S. Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: CAV \u201909: Proceedings of the 21st International Conference on Computer Aided Verification, vol. 5643 of LNCS, pp. 477\u2013492. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"276_CR29","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: CAV \u201910: Proceedings of the 22nd International Conference on Computer Aided Verification, vol. 6174 of LNCS, pp. 629\u2013644. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14295-6_54"},{"key":"276_CR30","doi-asserted-by":"crossref","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Sequentializing parameterized programs. In: FIT \u201912: Proceedings of the Fourth Workshop on Foundations of Interface Technologies, vol. 87 of EPTCS, pp. 34\u201347 (2012)","DOI":"10.4204\/EPTCS.87.4"},{"issue":"1","key":"276_CR31","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/s10703-009-0078-9","volume":"35","author":"A Lal","year":"2009","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Form. Methods Syst. Design 35(1), 73\u201397 (2009)","journal-title":"Form. Methods Syst. Design"},{"key":"276_CR32","doi-asserted-by":"crossref","unstructured":"Lal, A. Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: CAV \u201912: Proceedings of the 24th International Conference on Computer Aided Verification, vol. 7358 of LNCS, pp. 427\u2013443. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"276_CR33","unstructured":"Lynch, N.A.: Distributed algorithms. ISBN 1-55860-348-4. Morgan Kaufmann, San Francisco (1996)"},{"key":"276_CR34","doi-asserted-by":"crossref","unstructured":"Miller, M.S., Tribble, E.D., Shapiro, J.S.: Concurrency among strangers. In: TGC \u201905: Proceedings of the International Symposium on Trustworthy Global Computing, vol. 3705 of LNCS, pp. 195\u2013229. Springer, Heidelberg (2005)","DOI":"10.1007\/11580850_12"},{"issue":"4","key":"276_CR35","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"EL Post","year":"1946","unstructured":"Post, E.L.: A variant of a recursively unsolvable problem. Bull. Am. Math. Soc 52(4), 264\u2013268 (1946)","journal-title":"Bull. Am. Math. Soc"},{"key":"276_CR36","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: TACAS \u201905: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 3440 of LNCS, pp. 93\u2013107. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"276_CR37","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: PLDI \u201904: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 14\u201324. ACM, New York (2004)","DOI":"10.1145\/996841.996845"},{"key":"276_CR38","doi-asserted-by":"crossref","unstructured":"Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: POPL \u201995: Proceedings of the 22th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 49\u201361. ACM, New York (1995)","DOI":"10.1145\/199448.199462"},{"key":"276_CR39","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M.: Model checking multithreaded programs with asynchronous atomic methods. In: CAV \u201906: Proceedings of the 18th International Conference on Computer Aided Verification, vol. 4144 of LNCS, pp. 300\u2013314. Springer, Heidelberg (2006)","DOI":"10.1007\/11817963_29"},{"key":"276_CR40","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data-flow analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, chapter 7, pp. 189\u2013234. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"276_CR41","doi-asserted-by":"crossref","unstructured":"Svensson, H., Arts, T.: A new leader election implementation. In: Erlang \u201905: Proceedings of the 2005 ACM SIGPLAN Workshop on Erlang, pp. 35\u201339. ACM, New York (2005)","DOI":"10.1145\/1088361.1088368"},{"key":"276_CR42","unstructured":"Trottier-Hebert, F.: Learn you some Erlang for great good! http:\/\/learnyousomeerlang.com\/ . Accessed 1 Jan 2012"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0276-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0276-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0276-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,13]],"date-time":"2019-07-13T06:23:50Z","timestamp":1562999030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0276-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5,4]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["276"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0276-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5,4]]}}}