{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:33Z","timestamp":1763468133663},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642388552"},{"type":"electronic","value":"9783642388569"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38856-9_24","type":"book-chapter","created":{"date-parts":[[2013,6,15]],"date-time":"2013-06-15T00:05:28Z","timestamp":1371254728000},"page":"454-476","source":"Crossref","is-referenced-by-count":30,"title":["Automatic Verification of Erlang-Style Concurrency"],"prefix":"10.1007","author":[{"given":"Emanuele","family":"D\u2019Osualdo","sequence":"first","affiliation":[]},{"given":"Jonathan","family":"Kochems","sequence":"additional","affiliation":[]},{"given":"C. -H. Luke","family":"Ong","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"Actors: a model of concurrent computation in distributed systems","author":"G. Agha","year":"1986","unstructured":"Agha, G.: Actors: a model of concurrent computation in distributed systems. MIT Press, Cambridge (1986)"},{"issue":"9","key":"24_CR2","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1810891.1810910","volume":"53","author":"J. Armstrong","year":"2010","unstructured":"Armstrong, J.: Erlang. CACM\u00a053(9), 68 (2010)","journal-title":"CACM"},{"key":"24_CR3","unstructured":"Armstrong, J., Virding, R., Williams, M.: Concurrent programming in Erlang. Prentice Hall (1993)"},{"key":"24_CR4","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/640128.604137","volume":"38","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. ACM SIGPLAN Notices\u00a038, 62\u201373 (2003)","journal-title":"ACM SIGPLAN Notices"},{"key":"24_CR5","unstructured":"Carlsson, R.: An introduction to Core Erlang. In: Proceedings of the PLI 2001 Erlang Workshop (2001)"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Carlsson, R., Sagonas, K., Wilhelmsson, J.: Message analysis for concurrent programs using message passing. ACM TOPLAS (2006)","DOI":"10.1145\/1146809.1146813"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-11503-5_11","volume-title":"Practical Aspects of Declarative Languages","author":"M. Christakis","year":"2010","unstructured":"Christakis, M., Sagonas, K.: Static detection of race conditions in erlang. In: Carro, M., Pe\u00f1a, R. (eds.) PADL 2010. LNCS, vol.\u00a05937, pp. 119\u2013133. Springer, Heidelberg (2010)"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-18378-2_3","volume-title":"Practical Aspects of Declarative Languages","author":"M. Christakis","year":"2011","unstructured":"Christakis, M., Sagonas, K.: Detection of asynchronous message passing errors using static analysis. In: Rocha, R., Launchbury, J. (eds.) PADL 2011. LNCS, vol.\u00a06539, pp. 5\u201318. Springer, Heidelberg (2011)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Colby, C.: Analyzing the communication topology of concurrent programs. In: PEPM, pp. 202\u2013213 (1995)","DOI":"10.1145\/215465.215592"},{"key":"24_CR10","unstructured":"D\u2019Osualdo, E., Kochems, J., Ong, C.-H.L.: Verifying Erlang-style concurrency automatically. Technical report, University of Oxford DCS Technical Report (2011), http:\/\/mjolnir.cs.ox.ac.uk\/soter\/cpmrs.pdf"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"D\u2019Osualdo, E., Kochems, J., Ong, C.-H.L.: Soter: an automatic safety verifier for Erlang. In: AGERE! 2012, pp. 137\u2013140. ACM (2012)","DOI":"10.1145\/2414639.2414658"},{"key":"24_CR12","unstructured":"D\u2019Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of Erlang-style concurrency. CoRR, abs\/1303.2201 (2013), http:\/\/arxiv.org\/abs\/1303.2201"},{"issue":"1","key":"24_CR13","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.jlap.2004.01.005","volume":"63","author":"J. Feret","year":"2005","unstructured":"Feret, J.: Abstract interpretation of mobile systems. Journal of Logic and Algebraic Programming\u00a063(1), 59\u2013130 (2005)","journal-title":"Journal of Logic and Algebraic Programming"},{"issue":"1-2","key":"24_CR14","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science\u00a0256(1-2), 63\u201392 (2001)","journal-title":"Theoretical Computer Science"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Fredlund, L., Svensson, H.: McErlang: a model checker for a distributed functional programming language. In: ICFP, pp. 125\u2013136 (2007)","DOI":"10.1145\/1291220.1291171"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. TOPLAS\u00a034(1) (2012)","DOI":"10.1145\/2160910.2160915"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/11768869_8","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"P.-L. Garoche","year":"2006","unstructured":"Garoche, P.-L., Pantel, M., Thirioux, X.: Static safety for an actor dedicated process calculus by abstract interpretation. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol.\u00a04037, pp. 78\u201392. Springer, Heidelberg (2006)"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Huch, F.: Verification of Erlang programs using abstract interpretation and model checking. In: ICFP, pp. 261\u2013272 (1999)","DOI":"10.1145\/317765.317908"},{"key":"24_CR19","first-page":"339","volume-title":"POPL 2007","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL 2007, pp. 339\u2013350. ACM, New York (2007)"},{"key":"24_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-32940-1_35","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"A. Kaiser","year":"2012","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Efficient coverability analysis by proof minimization. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 500\u2013515. Springer, Heidelberg (2012), www.cprover.org\/bfc\/"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-60360-3_42","volume-title":"Static Analysis","author":"N. Kobayashi","year":"1995","unstructured":"Kobayashi, N., Nakade, M., Yonezawa, A.: Static analysis of communication for asynchronous concurrent programming languages. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol.\u00a0983, pp. 225\u2013242. Springer, Heidelberg (1995)"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Lindahl, T., Sagonas, K.: Practical type inference based on success typings. In: PPDP, pp. 167\u2013178 (2006)","DOI":"10.1145\/1140335.1140356"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Long, Z., Calin, G., Majumdar, R., Meyer, R.: Language-Theoretic abstraction refinement. In: de Lara, J., Zisman, A. (eds.) FASE. LNCS, vol.\u00a07212, pp. 362\u2013376. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28872-2_25"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Marlow, S., Wadler, P.: A practical subtyping system for Erlang. In: ICFP, pp. 136\u2013149 (1997)","DOI":"10.1145\/258949.258962"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Meyer, R.: On boundedness in depth in the \u03c0-calculus. In: Fifth Ifip International Conference On Theoretical Computer Science, pp. 477\u2013489 (2008)","DOI":"10.1007\/978-0-387-09680-3_32"},{"key":"24_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-69166-2_23","volume-title":"Static Analysis","author":"J. Midtgaard","year":"2008","unstructured":"Midtgaard, J., Jensen, T.: A calculational approach to control-flow analysis by abstract interpretation. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol.\u00a05079, pp. 347\u2013362. Springer, Heidelberg (2008)"},{"key":"24_CR27","doi-asserted-by":"crossref","unstructured":"Might, M., Van Horn, D.: A family of abstract interpretations for static analysis of concurrent higher-order programs. In: Yahav, E. (ed.) SAS. LNCS, vol.\u00a06887, pp. 180\u2013197. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-23702-7_16"},{"key":"24_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A calculus of communicating systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A calculus of communicating systems, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Nystr\u00f6m, S.: A soft-typing system for Erlang. In: ACM Sigplan Erlang Workshop, pp. 56\u201371 (2003)","DOI":"10.1145\/940880.940888"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: POPL, pp. 587\u2013598 (2011)","DOI":"10.1145\/1925844.1926453"},{"key":"24_CR31","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/143103.143125","volume":"27","author":"Y.G. Park","year":"1992","unstructured":"Park, Y.G., Goldberg, B.: Escape analysis on lists. ACM SIGPLAN Notices\u00a027, 116\u2013127 (1992)","journal-title":"ACM SIGPLAN Notices"},{"key":"24_CR32","unstructured":"Pike, R.: Concurrency and message passing in Newsqueak. Google Talks Archive, http:\/\/youtu.be\/hB05UFqOtFA"},{"key":"24_CR33","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. Theoretical Computer Science\u00a06, 223\u2013231 (1978)","journal-title":"Theoretical Computer Science"},{"key":"24_CR34","doi-asserted-by":"crossref","unstructured":"Reppy, J.H., Xiao, Y.: Specialization of CML message-passing primitives. In: POPL, pp. 315\u2013326 (2007)","DOI":"10.1145\/1190215.1190264"},{"key":"24_CR35","unstructured":"Shivers, O.: Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University (1991)"},{"key":"24_CR36","doi-asserted-by":"crossref","unstructured":"Van Horn, D., Might, M.: Abstracting abstract machines. In: ICFP, pp. 51\u201362 (2010)","DOI":"10.1145\/1932681.1863553"},{"key":"24_CR37","doi-asserted-by":"crossref","unstructured":"Venet, A.: Abstract interpretation of the pi-calculus. In: LOMAPS, pp. 51\u201375 (1996)","DOI":"10.1007\/3-540-62503-8_3"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38856-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,28]],"date-time":"2020-07-28T09:40:55Z","timestamp":1595929255000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38856-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388552","9783642388569"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38856-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}