{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:26:44Z","timestamp":1750307204642,"version":"3.41.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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 Comput. Surv."],"published-print":{"date-parts":[[2012,1]]},"abstract":"<jats:p>Flow Logic is an approach to statically determining the behavior of programs and processes. It borrows methods and techniques from Abstract Interpretation, Data Flow Analysis and Constraint Based Analysis while presenting the analysis in a style more reminiscent of Type Systems. Traditionally developed for programming languages, this article provides a tutorial development of the approach of Flow Logic for process calculi based on a decade of research.<\/jats:p>\n          <jats:p>\n            We first develop a simple analysis for the\n            <jats:italic>\u03c0<\/jats:italic>\n            -calculus; this consists of the specification, semantic soundness (in the form of subject reduction and adequacy results), and a Moore Family result showing that a least solution always exists, as well as providing insights on how to implement the analysis. We then show how to strengthen the analysis technology by introducing reachability components, interaction points, and localized environments, and finally, we extend it to a relational analysis.\n          <\/jats:p>\n          <jats:p>A Flow Logic is a program logic---in the same sense that a Hoare\u2019s logic is. We conclude with an executive summary presenting the highlights of the approach from this perspective including a discussion of theoretical properties as well as implementation considerations.<\/jats:p>\n          <jats:p>\n            The electronic supplements present an application of the analysis techniques to a version of the\n            <jats:italic>\u03c0<\/jats:italic>\n            -calculus incorporating distribution and code mobility; also the proofs of the main results can be found in the electronic supplements.\n          <\/jats:p>","DOI":"10.1145\/2071389.2071392","type":"journal-article","created":{"date-parts":[[2012,1,31]],"date-time":"2012-01-31T14:49:20Z","timestamp":1328021360000},"page":"1-39","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Flow Logic for Process Calculi"],"prefix":"10.1145","volume":"44","author":[{"given":"Hanne Riis","family":"Nielson","sequence":"first","affiliation":[{"name":"The Technical University of Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Flemming","family":"Nielson","sequence":"additional","affiliation":[{"name":"The Technical University of Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henrik","family":"Pilegaard","sequence":"additional","affiliation":[{"name":"The Technical University of Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,1]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2740"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/324133.324266"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"Apt K. Blair H. and Walker A. 1988. A theory of declarative programming. In Foundations of Deductive Databases and Logic Programming. Morgan-Kaufman 89--148. Apt K. Blair H. and Walker A. 1988. A theory of declarative programming. In Foundations of Deductive Databases and Logic Programming . Morgan-Kaufman 89--148.","DOI":"10.1016\/B978-0-934613-40-8.50006-3"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_3"},{"volume":"2874","volume-title":"Security and Analysis of Systems. Lecture Notes in Computer Science","author":"Bettini L.","key":"e_1_2_2_6_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/646733.701449"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/646791.756942"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.3020"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/645768.667616"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-739X(02)00047-X"},{"volume-title":"Proceedings of IEEE Computer Security Foundations Workshop (CSFW). IEEE Press, 126--140","author":"Bodei C.","key":"e_1_2_2_12_1"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1145948.1145950"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1066473.1066476"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.09.010"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770176.1770183"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/645870.668676"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00231-5"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90032-X"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.685256"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1788954.1788961"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2009.07.009"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/645396.651966"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1759210.1759224"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/647168.718142"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2006.115"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2008.162"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Hennessy M. 2007. A Distributed Pi-Calculus. Cambridge University Press Cambridge UK. Hennessy M. 2007. A Distributed Pi-Calculus . Cambridge University Press Cambridge UK.","DOI":"10.1017\/CBO9780511611063"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/596980.596981"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/647168.718136"},{"key":"e_1_2_2_31_1","unstructured":"Milner R. 1999. Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press Cambridge UK. Milner R. 1999. Communicating and Mobile Systems: the Pi-Calculus . Cambridge University Press Cambridge UK."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.018"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_14"},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Nielson F. Nielson H. R. and Hankin C. L. 1999. Principles of Program Analysis. Springer. Nielson F. Nielson H. R. and Hankin C. L. 1999. Principles of Program Analysis . Springer.","DOI":"10.1007\/978-3-662-03811-6"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00140-2"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00316-0"},{"key":"e_1_2_2_37_1","first-page":"335","article-title":"A Succinct solver for ALFP","volume":"9","author":"Nielson F.","year":"2002","journal-title":"Nordic J. Comput."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.01.041"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1793574.1793583"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/860256.860268"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.4"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2008.07.001"},{"key":"e_1_2_2_43_1","doi-asserted-by":"crossref","unstructured":"Nielson H. R. Nielson F. and Pilegaard H. 2004. Spatial analysis of BioAmbients. In Proceedings of the International Static Analysis Symposium (SAS). Lecture Notes in Computer Science. Springer 69--83. Nielson H. R. Nielson F. and Pilegaard H. 2004. Spatial analysis of BioAmbients. In Proceedings of the International Static Analysis Symposium (SAS). Lecture Notes in Computer Science. Springer 69--83.","DOI":"10.1007\/978-3-540-27864-1_8"},{"key":"e_1_2_2_44_1","doi-asserted-by":"crossref","unstructured":"Nielson H. R. Nielson F. and \n      \n      \n      Buchholtz M\n      \n  \n  . \n  2005\n  . Security for mobility. In Foundations of Security Analysis and Design II R. Focardi and R. Gorrieri Eds. Lecture Notes in Computer Science vol. \n  2946 Springer 207--266. Nielson H. R. Nielson F. and Buchholtz M. 2005. Security for mobility. In Foundations of Security Analysis and Design II R. Focardi and R. Gorrieri Eds. Lecture Notes in Computer Science vol. 2946 Springer 207--266.","DOI":"10.1007\/978-3-540-24631-2_6"},{"volume-title":"Handbook of Process Algebra","author":"Parrow J.","key":"e_1_2_2_45_1"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.09.014"},{"volume-title":"Proceedings of the 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI).","author":"Pilegaard H.","key":"e_1_2_2_47_1"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.05.006"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/1777688.1777697"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.03.061"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54007"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1777688.1777701"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.5555\/647167.717991"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071389.2071392","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2071389.2071392","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:06:22Z","timestamp":1750241182000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071389.2071392"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["10.1145\/2071389.2071392"],"URL":"https:\/\/doi.org\/10.1145\/2071389.2071392","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"type":"print","value":"0360-0300"},{"type":"electronic","value":"1557-7341"}],"subject":[],"published":{"date-parts":[[2012,1]]},"assertion":[{"value":"2009-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}