{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,23]],"date-time":"2026-09-23T06:31:01Z","timestamp":1790145061405,"version":"4.0.1"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>Abstract interpretation is a methodology for defining sound static analysis. Yet, building sound static analyses for modern programming languages is difficult, because these static analyses need to combine sophisticated abstractions for values, environments, stores, etc. However, static analyses often tightly couple these abstractions in the implementation, which not only complicates the implementation, but also makes it hard to decide which parts of the analyses can be proven sound independently from each other. Furthermore, this coupling makes it hard to combine soundness lemmas for parts of the analysis to a soundness proof of the complete analysis.<\/jats:p>\n          <jats:p>\n            To solve this problem, we propose to construct static analyses modularly from\n            <jats:italic>reusable analysis components<\/jats:italic>\n            . Each analysis component encapsulates a single analysis concern and can be proven sound independently from the analysis where it is used. We base the design of our analysis components on\n            <jats:italic>arrow transformers<\/jats:italic>\n            , which allows us to compose analysis components. This composition preserves soundness, which guarantees that a static analysis is sound, if all its analysis components are sound. This means that analysis developers do not have to worry about soundness as long as they reuse sound analysis components. To evaluate our approach, we developed a library of 13 reusable analysis components in Haskell. We use these components to define a\n            <jats:italic>k<\/jats:italic>\n            -CFA analysis for PCF and an interval and reaching definition analysis for a While language.\n          <\/jats:p>","DOI":"10.1145\/3360602","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Sound and reusable components for abstract interpretation"],"prefix":"10.1145","volume":"3","author":[{"given":"Sven","family":"Keidel","sequence":"first","affiliation":[{"name":"Johannes Gutenberg University Mainz, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian","family":"Erdweg","sequence":"additional","affiliation":[{"name":"Johannes Gutenberg University Mainz, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"The Calculational Design of a Generic Abstract Interpreter","author":"Cousot P."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_2_3_1","volume-title":"4th International Symposium, PLILP\u201992","author":"Cousot Patrick","year":"1992"},{"key":"e_1_2_2_4_1","volume-title":"ICFP","author":"Darais David","year":"2017"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814308"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_2_7_1","volume-title":"Proceedings of the 3rd ACM SIGPLAN Symposium on Haskell, Haskell 2010","author":"Ed Jeremy Gibbons","year":"2010"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"e_1_2_2_9_1","volume-title":"Proceedings of the seventh ACM SIGPLAN workshop on Generic programming, WGP@ICFP 2011","author":"Hamana Makoto","year":"2011"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863553"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_2_2_13_1","volume-title":"Casper Bach Poulsen, and Sebastian Erdweg","author":"Keidel Sven","year":"2018"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Jens Knoop and Oliver R\u00fcthing. 1999. Optimization Under the Perspective of Soundness Completeness and Reusability. In Correct System Design Recent Insight and Advances (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel). 288\u2013315.  Jens Knoop and Oliver R\u00fcthing. 1999. Optimization Under the Perspective of Soundness Completeness and Reusability. In Correct System Design Recent Insight and Advances (to Hans Langmaack on the occasion of his retirement from his professorship at the University of Kiel). 288\u2013315.","DOI":"10.1007\/3-540-48092-7_13"},{"key":"e_1_2_2_15_1","volume-title":"Monad Transformers and Modular Interpreters. In Conference Record of POPL\u201995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Liang Sheng","year":"1995"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213847"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384660"},{"key":"e_1_2_2_18_1","volume-title":"Hanne Riis Nielson, and Chris Hankin","author":"Nielson Flemming","year":"1999"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1944-0010555-7"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/361598.361623"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507664"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2004.1"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491979"},{"key":"e_1_2_2_26_1","volume-title":"APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings. 485\u2013503","author":"Smaragdakis Yannis","year":"2015"},{"key":"e_1_2_2_27_1","volume-title":"Third International Symposium, SAS\u201996","author":"Venet Arnaud","year":"1996"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360602","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360602","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360602"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":26,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360602"],"URL":"https:\/\/doi.org\/10.1145\/3360602","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}