{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:40Z","timestamp":1759638940061},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319024431"},{"type":"electronic","value":"9783319024448"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-319-02444-8_20","type":"book-chapter","created":{"date-parts":[[2013,8,29]],"date-time":"2013-08-29T01:11:21Z","timestamp":1377738681000},"page":"272-286","source":"Crossref","is-referenced-by-count":7,"title":["Analysis of Message Passing Programs Using SMT-Solvers"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"given":"Jonathan","family":"Cederberg","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/3-540-58201-0_78","volume-title":"Automata, Languages, and Programming","author":"P. Abdulla","year":"1994","unstructured":"Abdulla, P., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol.\u00a0820, pp. 316\u2013327. Springer, Heidelberg (1994)"},{"key":"20_CR2","unstructured":"Abdulla, P.A., Atig, M.F., Cederberg, J.: Alternator - Verifier of programs by bounding mode alternations, \n                    \n                      https:\/\/github.com\/it-apv\/alternator"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-28756-5_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2012","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 204\u2013219. Springer, Heidelberg (2012)"},{"issue":"1","key":"20_CR4","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/B:FORM.0000033962.51898.1a","volume":"25","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. Formal Methods in System Design\u00a025(1), 39\u201365 (2004)","journal-title":"Formal Methods in System Design"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: Proc. LICS 1993, 8th IEEE Int. Symp. on Logic in Computer Science, pp. 160\u2013170 (1993)","DOI":"10.1109\/LICS.1993.287591"},{"key":"20_CR6","unstructured":"Barrett, C., et al.: The smt-lib standard: Version 2.0. Tech. rep. (2010)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL, pp. 7\u201318. ACM (2010)","DOI":"10.1145\/1706299.1706303"},{"key":"20_CR8","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)"},{"issue":"3","key":"20_CR9","first-page":"237","volume":"14","author":"B. Boigelot","year":"1999","unstructured":"Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using qdds. FMSD\u00a014(3), 237\u2013255 (1999)","journal-title":"FMSD"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-642-28756-5_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2012","unstructured":"Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 451\u2013465. Springer, Heidelberg (2012)"},{"key":"20_CR11","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, pp. 62\u201373. ACM (2003)","DOI":"10.1145\/604131.604137"},{"issue":"1-2","key":"20_CR12","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":"20_CR13","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":"20_CR14","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: STOC, pp. 151\u2013158. ACM (1971)","DOI":"10.1145\/800157.805047"},{"issue":"1","key":"20_CR15","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1016\/j.jcss.2005.09.001","volume":"72","author":"G. Geeraerts","year":"2006","unstructured":"Geeraerts, G., Raskin, J.F., Begin, L.V.: Expand, enlarge and check: New algorithms for the coverability problem of wsts. J. Comput. Syst. Sci.\u00a072(1), 180\u2013203 (2006)","journal-title":"J. Comput. Syst. Sci."},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-31424-7_22","volume-title":"Computer Aided Verification","author":"M. Hague","year":"2012","unstructured":"Hague, M., Lin, A.W.: Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 260\u2013276. Springer, Heidelberg (2012)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Heu\u00dfner, A., Leroux, J., Muscholl, A., Sutre, G.: Reachability analysis of communicating pushdown systems. Logical Methods in Computer Science\u00a08(3) (2012)","DOI":"10.2168\/LMCS-8(3:23)2012"},{"issue":"1","key":"20_CR18","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/322047.322058","volume":"25","author":"O.H. Ibarra","year":"1978","unstructured":"Ibarra, O.H.: Reversal-bounded multicounter machines and their decision problems. J. ACM\u00a025(1), 116\u2013133 (1978)","journal-title":"J. ACM"},{"key":"20_CR19","unstructured":"Marques Jr., A.P., Ravn, A., Srba, J., Vighio, S.: csv2uppaal, \n                    \n                      https:\/\/github.com\/csv2uppaal"},{"key":"20_CR20","unstructured":"Lipton, R.: The reachability problem requires exponential time. Technical Report TR 66 (1976)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"6","key":"20_CR22","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1145\/1273442.1250785","volume":"42","author":"Madanlal Musuvathi","year":"2007","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI, pp. 446\u2013455. ACM (2007)","journal-title":"ACM SIGPLAN Notices"},{"key":"20_CR23","unstructured":"Newcomer, E., Robinson, I. (chairs): Web Services Business Activity Version 1.2 (2009), \n                    \n                      http:\/\/docs.oasis-open.org\/ws-tx\/wstx-wsba-1.2-spec-os.pdf"},{"key":"20_CR24","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":"20_CR25","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C. Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci.\u00a06, 223\u2013231 (1978)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-19835-9_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A.P. Ravn","year":"2011","unstructured":"Ravn, A.P., Srba, J., Vighio, S.: Modelling and verification of web services business activity protocol. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 357\u2013371. Springer, Heidelberg (2011)"},{"issue":"1","key":"20_CR27","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1109\/MMUL.2007.14","volume":"14","author":"P. Saint-Andre","year":"2007","unstructured":"Saint-Andre, P.: Jingle: Jabber does multimedia. IEEE MultiMedia\u00a014(1), 90\u201394 (2007)","journal-title":"IEEE MultiMedia"},{"issue":"5","key":"20_CR28","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0020-0190(01)00337-4","volume":"83","author":"P. Schnoebelen","year":"2002","unstructured":"Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters\u00a083(5), 251\u2013261 (2002)","journal-title":"Information Processing Letters"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1136","DOI":"10.1007\/978-3-540-27836-8_94","volume-title":"Automata, Languages and Programming","author":"H. Seidl","year":"2004","unstructured":"Seidl, H., Schwentick, T., Muscholl, A., Habermehl, P.: Counting in trees for free. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 1136\u20131149. Springer, Heidelberg (2004)"},{"key":"20_CR30","unstructured":"The Erlang Programming Language, \n                    \n                      http:\/\/erlang.org"},{"key":"20_CR31","unstructured":"The Scala Programming Language, \n                    \n                      http:\/\/scala-lang.org"},{"key":"20_CR32","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)"}],"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-319-02444-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,28]],"date-time":"2019-01-28T07:12:34Z","timestamp":1548659554000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-02444-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319024431","9783319024448"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-02444-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}