{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T07:01:53Z","timestamp":1767855713490,"version":"3.49.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["FA875016-2-0032."],"award-info":[{"award-number":["FA875016-2-0032."]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>Abstract interpretation promises sound but computable static summarization of program behavior. However, modern software engineering practices pose significant challenges to this vision, specifically the extensive use of frameworks and complex libraries. Frameworks heavily use reflection, metaprogramming, and multiple layers of abstraction, all of which confound even state-of-the-art abstract interpreters. Sound but conservative analysis of frameworks is impractically imprecise, and unsoundly ignoring reflection and metaprogramming is untenable given the prevalence of these features. Manually modeling framework behaviors offers excellent precision, at the cost of immense effort by the tool designer.<\/jats:p>\n          <jats:p>To overcome the above difficulties, we present Concerto, a system for analyzing framework-based applications by soundly combining concrete and abstract interpretation. Concerto analyzes framework implementations using concrete interpretation, and application code using abstract interpretation. This technique is possible in practice as framework implementations typically follow a single path of execution when provided a concrete, application-specific configuration file which is often available at analysis time. Concerto exploits this configuration information to precisely resolve reflection and other metaprogramming idioms during concrete execution. In contrast, application code may have infinitely many paths of execution, so Concerto switches to abstract interpretation to analyze application code. Concerto is an analysis framework, and can be instantiated with any abstract interpretation that satisfies a small set of preconditions. In addition, unlike manual modeling, Concerto is not specialized to any specific framework implementation. We have formalized our approach and proved several important properties including soundness and termination. In addition, we have implemented an initial proof of concept prototype of Concerto for a subset of Java, and found that our combined interpretation significantly improves analysis precision and performance.<\/jats:p>","DOI":"10.1145\/3290356","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Concerto: a framework for combined concrete and abstract interpretation"],"prefix":"10.1145","volume":"3","author":[{"given":"John","family":"Toman","sequence":"first","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dan","family":"Grossman","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594299"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568293"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.22"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Paulo Barros Ren\u00e9 Just Suzanne Millstein Paul Vines Werner Dietl Michael D Ernst etal 2015. Static analysis of implicit control flow: Resolving Java reflection and Android intents. In ASE.  Paulo Barros Ren\u00e9 Just Suzanne Millstein Paul Vines Werner Dietl Michael D Ernst et al. 2015. Static analysis of implicit control flow: Resolving Java reflection and Android intents. In ASE.","DOI":"10.1109\/ASE.2015.69"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771284.2771288"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985827"},{"key":"e_1_2_2_7_1","unstructured":"Fran\u00e7ois Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings. In Formal Methods in Programming and their Applications .  Fran\u00e7ois Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings. In Formal Methods in Programming and their Applications ."},{"key":"e_1_2_2_8_1","volume-title":"Workshop on Advances in Verification.","author":"Brat Guillaume","year":"2000","unstructured":"Guillaume Brat , Klaus Havelund , SeungJoon Park , and Willem Visser . 2000 . Java PathFinder-second generation of a Java model checker . In Workshop on Advances in Verification. Guillaume Brat, Klaus Havelund, SeungJoon Park, and Willem Visser. 2000. Java PathFinder-second generation of a Java model checker. In Workshop on Advances in Verification."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1811212.1811216"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158102"},{"key":"e_1_2_2_11_1","volume-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI.","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , Dawson R Engler , 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI. Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961295.1950396"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542483"},{"key":"e_1_2_2_14_1","volume-title":"Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Res. rep. RR 88","author":"Cousot Patrick","year":"1977","unstructured":"Patrick Cousot . 1977. Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Res. rep. RR 88 ( 1977 ). Patrick Cousot. 1977. Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Res. rep. RR 88 (1977)."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_16_1","volume-title":"Constructive versions of Tarski\u2019s fixed point theorems. Pacific journal of Mathematics 82, 1","author":"Cousot Patrick","year":"1979","unstructured":"Patrick Cousot and Radhia Cousot . 1979a. Constructive versions of Tarski\u2019s fixed point theorems. Pacific journal of Mathematics 82, 1 ( 1979 ). Patrick Cousot and Radhia Cousot. 1979a. Constructive versions of Tarski\u2019s fixed point theorems. Pacific journal of Mathematics 82, 1 (1979)."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_2_2_20_1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot Radhia Cousot J\u00e9r\u00f4me Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2005. The ASTR\u00c9E analyzer. In ESOP.  Patrick Cousot Radhia Cousot J\u00e9r\u00f4me Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2005. The ASTR\u00c9E analyzer. In ESOP.","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_2_2_21_1","volume-title":"Annual Asian Computing Science Conference.","author":"Cousot Patrick","year":"2006","unstructured":"Patrick Cousot , Radhia Cousot , J\u00e9r\u00f4me Feret , Laurent Mauborgne , Antoine Min\u00e9 , David Monniaux , and Xavier Rival . 2006 . Combination of abstractions in the ASTR\u00c9E static analyzer . In Annual Asian Computing Science Conference. Patrick Cousot, Radhia Cousot, J\u00e9r\u00f4me Feret, Laurent Mauborgne, Antoine Min\u00e9, David Monniaux, and Xavier Rival. 2006. Combination of abstractions in the ASTR\u00c9E static analyzer. In Annual Asian Computing Science Conference."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1348250.1348254"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360056"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178263"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273463.1273480"},{"key":"e_1_2_2_26_1","doi-asserted-by":"crossref","unstructured":"Manuel F\u00e4hndrich and Francesco Logozzo. 2010. Static contract checking with abstract interpretation. In Formal Verification of Object-Oriented Software .  Manuel F\u00e4hndrich and Francesco Logozzo. 2010. Static contract checking with abstract interpretation. In Formal Verification of Object-Oriented Software .","DOI":"10.1007\/978-3-642-18070-5_2"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13464-7_15"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_17"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1348250.1348255"},{"key":"e_1_2_2_30_1","unstructured":"Martin Fowler. 2004. Inversion of control containers and the dependency injection pattern. (2004).  Martin Fowler. 2004. Inversion of control containers and the dependency injection pattern. (2004)."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010095604496"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133892"},{"key":"e_1_2_2_34_1","unstructured":"Neil D Jones Carsten K Gomard and Peter Sestoft. 1993. Partial evaluation and automatic program generation. Peter Sestoft.   Neil D Jones Carsten K Gomard and Peter Sestoft. 1993. Partial evaluation and automatic program generation. Peter Sestoft."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567776"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00290339"},{"key":"e_1_2_2_37_1","unstructured":"Yoonseok Ko Hongki Lee Julian Dolby and Sukyoung Ryu. 2015. Practically Tunable Static Analysis Framework for LargeScale JavaScript Applications. In ASE.  Yoonseok Ko Hongki Lee Julian Dolby and Sukyoung Ryu. 2015. Practically Tunable Static Analysis Framework for LargeScale JavaScript Applications. In ASE."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328408.1328410"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_20"},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Yue Li Tian Tan and Jingling Xue. 2015. Effective soundness-guided reflection analysis. In SAS.  Yue Li Tian Tan and Jingling Xue. 2015. Effective soundness-guided reflection analysis. In SAS.","DOI":"10.1007\/978-3-662-48288-9_10"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1363686.1363736"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/215465.215469"},{"key":"e_1_2_2_43_1","volume-title":"4th Hungarian Computer Science Conference . 211\u2013225","author":"Nielson Flemming","year":"1985","unstructured":"Flemming Nielson . 1985 . Tensor products generalize the relational data flow analysis method . In 4th Hungarian Computer Science Conference . 211\u2013225 . Flemming Nielson. 1985. Tensor products generalize the relational data flow analysis method. In 4th Hungarian Computer Science Conference . 211\u2013225."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908127"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_38"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_2_2_47_1","doi-asserted-by":"crossref","unstructured":"Yannis Smaragdakis George Balatsouras George Kastrinis and Martin Bravenboer. 2015. More sound static handling of Java reflection. In ASPLAS.  Yannis Smaragdakis George Balatsouras George Kastrinis and Martin Bravenboer. 2015. More sound static handling of Java reflection. In ASPLAS.","DOI":"10.1007\/978-3-319-26529-2_26"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048145"},{"key":"e_1_2_2_49_1","doi-asserted-by":"crossref","unstructured":"Gregory T Sullivan. 2001. Dynamic partial evaluation. In Programs as Data Objects. 238\u2013256.   Gregory T Sullivan. 2001. Dynamic partial evaluation. In Programs as Data Objects. 238\u2013256.","DOI":"10.1007\/3-540-44978-7_14"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/353171.353189"},{"key":"e_1_2_2_51_1","volume-title":"A lattice-theoretical fixpoint theorem and its applications. Pacific journal of Mathematics 5, 2","author":"Tarski Alfred","year":"1955","unstructured":"Alfred Tarski . 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific journal of Mathematics 5, 2 ( 1955 ). Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific journal of Mathematics 5, 2 (1955)."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_23"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2483760.2483788"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2245276.2231983"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290356","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290356","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290356","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290356"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290356"],"URL":"https:\/\/doi.org\/10.1145\/3290356","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}