{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:16:51Z","timestamp":1771024611375,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642287558","type":"print"},{"value":"9783642287565","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28756-5_31","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:57:15Z","timestamp":1332449835000},"page":"451-465","source":"Crossref","is-referenced-by-count":26,"title":["Bounded Phase Analysis of Message-Passing Programs"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Emmi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","unstructured":"HTML5: A vocabulary and associated APIs for HTML and XHTML, http:\/\/dev.w3.org\/html5\/spec\/Overview.html"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: LICS 1993: Proc. 8th Annual IEEE Symposium on Logic in Computer Science, pp. 160\u2013170. IEEE Computer Society (1993)","DOI":"10.1109\/LICS.1993.287591"},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"1998","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 305\u2013318. Springer, Heidelberg (1998)"},{"key":"31_CR4","unstructured":"Barnett, M., Leino, K.R.M., Moskal, M., Schulte, W.: Boogie: An intermediate verification language, http:\/\/research.microsoft.com\/en-us\/projects\/boogie\/"},{"issue":"3","key":"31_CR5","doi-asserted-by":"publisher","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. Formal Methods in System Design\u00a014(3), 237\u2013255 (1999)","journal-title":"Formal Methods in System Design"},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs (2011), http:\/\/hal.archives-ouvertes.fr\/hal-00653085\/en","DOI":"10.1007\/978-3-642-28756-5_31"},{"issue":"1-2","key":"31_CR7","doi-asserted-by":"publisher","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.\u00a0221(1-2), 211\u2013250 (1999)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"31_CR8","doi-asserted-by":"publisher","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. Formal Methods in System Design\u00a032(2), 129\u2013172 (2008)","journal-title":"Formal Methods in System Design"},{"key":"31_CR9","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-23702-7_13"},{"issue":"2","key":"31_CR10","doi-asserted-by":"publisher","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\u00a030(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"key":"31_CR11","unstructured":"Dahl, R.: Node.js: Evented I\/O for V8 JavaScript, http:\/\/nodejs.org\/"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Emmi, M., Qadeer, S., Rakamari\u0107, Z.: Delay-bounded scheduling. In: POPL 2011: Proc. 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 411\u2013422. ACM (2011)","DOI":"10.1145\/1926385.1926432"},{"key":"31_CR13","unstructured":"Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. CoRR, abs\/1011.0551 (2010), http:\/\/arxiv.org\/abs\/1011.0551"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL 2007: Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 339\u2013350. ACM (2007)","DOI":"10.1145\/1190216.1190266"},{"key":"31_CR15","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: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol.\u00a06349, pp. 245\u2013261. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-16164-3_18"},{"key":"31_CR16","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. La Torre","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":"31_CR17","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)"},{"issue":"1","key":"31_CR18","doi-asserted-by":"publisher","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. Formal Methods in System Design\u00a035(1), 73\u201397 (2009)","journal-title":"Formal Methods in System Design"},{"key":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/11580850_12","volume-title":"Trustworthy Global Computing","author":"M.S. Miller","year":"2005","unstructured":"Miller, M.S., Tribble, E.D., Shapiro, J.S.: Concurrency Among Strangers. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol.\u00a03705, pp. 195\u2013229. Springer, Heidelberg (2005)"},{"issue":"4","key":"31_CR20","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"E.L. Post","year":"1946","unstructured":"Post, E.L.: A variant of a recursively unsolvable problem. Bull. Amer. Math. Soc.\u00a052(4), 264\u2013268 (1946)","journal-title":"Bull. Amer. Math. Soc."},{"key":"31_CR21","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":"31_CR22","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: Keep it simple and sequential. In: PLDI 2004: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 14\u201324. ACM (2004)","DOI":"10.1145\/996841.996845"},{"key":"31_CR23","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":"31_CR24","doi-asserted-by":"crossref","unstructured":"Svensson, H., Arts, T.: A new leader election implementation. In: Erlang 2005: Proc. ACM SIGPLAN Workshop on Erlang, pp. 35\u201339. ACM (2005)","DOI":"10.1145\/1088361.1088368"},{"key":"31_CR25","unstructured":"Trottier-Hebert, F.: Learn you some Erlang for great good!, http:\/\/learnyousomeerlang.com\/"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28756-5_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:53:43Z","timestamp":1742756023000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28756-5_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642287558","9783642287565"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28756-5_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}