{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:06:27Z","timestamp":1776373587327,"version":"3.51.2"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,12,22]],"date-time":"2015-12-22T00:00:00Z","timestamp":1450742400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2016,3,28]]},"abstract":"<jats:p>\n            This article presents a\n            <jats:italic>may-happen-in-parallel<\/jats:italic>\n            (MHP) analysis for languages with\n            <jats:italic>actor-based concurrency<\/jats:italic>\n            . In this concurrency model, actors are the concurrency\n            <jats:italic>units<\/jats:italic>\n            such that, when a method is invoked on an actor\n            <jats:italic>a<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            from a task executing on actor\n            <jats:italic>a<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            , statements of the current task in\n            <jats:italic>a<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            may run in parallel with those of the (asynchronous) call on\n            <jats:italic>a<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            , and with those of transitively invoked methods. The goal of the MHP analysis is to identify pairs of statements in the program that may run in parallel in any execution. Our MHP analysis is formalized as a method-level (\n            <jats:italic>local<\/jats:italic>\n            ) analysis whose information can be modularly composed to obtain application-level (\n            <jats:italic>global<\/jats:italic>\n            ) information. The information yielded by the MHP analysis is essential to infer more complex properties of actor-based concurrent programs, for example, data race detection, deadlock freeness, termination, and resource consumption analyses can greatly benefit from the MHP relations to increase their accuracy. We report on MayPar, a prototypical implementation of an MHP static analyzer for a distributed asynchronous language.\n          <\/jats:p>","DOI":"10.1145\/2824255","type":"journal-article","created":{"date-parts":[[2015,12,23]],"date-time":"2015-12-23T15:19:49Z","timestamp":1450883989000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["May-Happen-in-Parallel Analysis for Actor-Based Concurrency"],"prefix":"10.1145","volume":"17","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[{"name":"Universidad Complutense de Madrid"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonio","family":"Flores-Montoya","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Darmstadt"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[{"name":"Universidad Complutense de Madrid"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrique","family":"Martin-Martin","sequence":"additional","affiliation":[{"name":"Universidad Complutense de Madrid"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,12,22]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229428.1229471"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/7929"},{"key":"e_1_2_2_3_1","unstructured":"A. V. Aho R. Sethi and J. D. Ullman. 1986. Compilers -- Principles Techniques and Tools. Addison-Wesley New York NY.   A. V. Aho R. Sethi and J. D. Ullman. 1986. Compilers -- Principles Techniques and Tools. Addison-Wesley New York NY."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_46"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_2"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30793-5_3"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02444-8_25"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_5"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69330-7_11"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/214037.214100"},{"key":"e_1_2_2_11_1","volume-title":"Lecture Notes in Computer Science","volume":"5930","author":"Clarke Dave","year":"2010"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250771"},{"key":"e_1_2_2_13_1","first-page":"185","article-title":"A constructive characterization of the lattices of all retractions, pre-closure, quasi-closure and closure operators on a complete lattice","volume":"38","author":"Cousot P.","year":"1979","journal-title":"Portugali\u00e6Mathematica"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762205"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/120807.120811"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393652"},{"key":"e_1_2_2_17_1","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Techniques for Distributed Systems (FMOODS\/FORTE\u201913)","author":"Flores-Montoya Antonio"},{"key":"e_1_2_2_18_1","volume-title":"Proceedings of the 20th International Symposium on Static Analysis, SAS 2013, Francesco Logozzo and Manuel F\u00e4hndrich (Eds.)","volume":"7935","author":"Gange Graeme"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.09.019"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512946"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25271-6_8"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/321921.321938"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_4"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1693453.1693459"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532378_15"},{"key":"e_1_2_2_26_1","unstructured":"Stephen P. Masticola. 1993. Static Detection of Deadlocks In Polynomial Time. Ph.D. Dissertation. Rutgers University New Brunswick NJ USA. http:\/\/dl.acm.org\/citation.cfm?id&equals;194282&CFID&equals;&equals;568373654&CFTOKEN&equals;&equals;93584834.   Stephen P. Masticola. 1993. Static Detection of Deadlocks In Polynomial Time. Ph.D. Dissertation. Rutgers University New Brunswick NJ USA. http:\/\/dl.acm.org\/citation.cfm?id&equals;194282&CFID&equals;&equals;568373654&CFTOKEN&equals;&equals;93584834."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/155332.155346"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566174"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070538"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/291252.288213"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/318774.319252"},{"key":"e_1_2_2_32_1","unstructured":"F. Nielson H. R. Nielson and C. Hankin. 2005. Principles of Program Analysis (2nd ed.). Springer.  F. Nielson H. R. Nielson and C. Hankin. 2005. Principles of Program Analysis (2nd ed.). Springer."},{"key":"e_1_2_2_33_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Theory and Practice of Parallel Programming, International Workshop TPPP\u201994, Sendai, Japan, November 7--9","author":"Pierce Benjamin C.","year":"1994"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_17"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00263928"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996859"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2824255","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2824255","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:43:22Z","timestamp":1750225402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2824255"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,22]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,3,28]]}},"alternative-id":["10.1145\/2824255"],"URL":"https:\/\/doi.org\/10.1145\/2824255","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,22]]},"assertion":[{"value":"2014-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-12-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}