{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,20]],"date-time":"2025-10-20T18:15:00Z","timestamp":1760984100380,"version":"3.41.2"},"reference-count":31,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,5,1]],"date-time":"2011-05-01T00:00:00Z","timestamp":1304208000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>In a functional language, the dominant control-flow mechanism is function call and return. Most higher-order flow analyses, including k-CFA, do not handle call and return well: they remember only a bounded number of pending calls because they approximate programs with control-flow graphs. Call\/return mismatch introduces precision-degrading spurious control-flow paths and increases the analysis time. We describe CFA2, the first flow analysis with precise call\/return matching in the presence of higher-order functions and tail calls. We formulate CFA2 as an abstract interpretation of programs in continuation-passing style and describe a sound and complete summarization algorithm for our abstract semantics. A preliminary evaluation shows that CFA2 gives more accurate data-flow information than 0CFA and 1CFA.<\/jats:p>","DOI":"10.2168\/lmcs-7(2:3)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:17:26Z","timestamp":1316780246000},"source":"Crossref","is-referenced-by-count":22,"title":["CFA2: a Context-Free Approach to Control-Flow Analysis"],"prefix":"10.46298","volume":"Volume 7, Issue 2","author":[{"given":"Dimitrios","family":"Vardoulakis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olin","family":"Shivers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2011,5,1]]},"reference":[{"key":"10.2168\/LMCS-7(2:3)2011_conf\/ecoop\/95\/agesen\/cpa","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49538-X_2"},{"issue":"4","key":"10.2168\/LMCS-7(2:3)2011_journal\/toplas\/05\/alur\/rsm","doi-asserted-by":"crossref","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"Rajeev Alur, Michael Benedikt, Kousha Et","year":"2005","journal-title":"Transactions on Programming Languages and Systems 27(4):786-818, 2005"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/concur\/97\/bouajjani\/pds","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability Analysis of Pushdown Automata: Application to Model-Checking. InInternational Conference on Concurrency Theory, pages 135-150, 1997.","DOI":"10.1007\/3-540-63141-0_10"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/pldi\/09\/chandra\/snugglebug","doi-asserted-by":"crossref","unstructured":"Satish Chandra, Stephen J. Fink, and Manu Sridharan. Snugglebug: a powerful approach to weakest preconditions. InProgramming Language Design and Implementation, pages 363-374, 2009.","DOI":"10.1145\/1543135.1542517"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/popl\/08\/chaudhuri\/subcubic","doi-asserted-by":"crossref","unstructured":"Swarat Chaudhuri. Subcubic Algorithms for Recursive State Machines. InPrinciples of Programming Languages, pages 159-169, 2008.","DOI":"10.1145\/1328897.1328460"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/lfp\/94\/clinger\/larceny","doi-asserted-by":"crossref","unstructured":"William D. Clinger and Lars Thomas Hansen. Lambda, the Ultimate Label or a Simple Optimizing Compiler for Scheme. InLISP and Functional Programming, pages 128-139, 1994.","DOI":"10.1145\/182590.156786"},{"issue":"4","key":"10.2168\/LMCS-7(2:3)2011_journal\/toplas\/97\/debray\/tailcall","doi-asserted-by":"crossref","first-page":"568","DOI":"10.1145\/262004.262006","volume":"19","author":"Saumya K. Debray and Todd A. Proebsting","year":"1997","journal-title":"Transactions on Programming Languages and Systems 19(4):568-585, 1997"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/sfp\/10\/earl\/pdcfa","unstructured":"Christopher Earl, Matthew Might, and David Van Horn. Pushdown Control-Flow Analysis of Higher-Order Programs. InWorkshop on Scheme and Functional Programming, 2010."},{"issue":"5","key":"10.2168\/LMCS-7(2:3)2011_journal\/mscs\/08\/fahndrich\/typeflow","doi-asserted-by":"crossref","first-page":"823","DOI":"10.1017\/S0960129508006968","volume":"18","author":"Manuel F\u00e4hndrich and Jakob Rehof","year":"2008","journal-title":"Mathematical Structures in Computer Science 2008"},{"key":"10.2168\/LMCS-7(2:3)2011_journal\/entcs\/97\/finkel\/pds","doi-asserted-by":"crossref","unstructured":"Alain Finkel, Bernard Willems, and Pierre Wolper. A direct symbolic approach to model checking pushdown systems.Electronic Notes in Theoretical Computer Science, 9, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/pldi\/93\/flanagan\/anf","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The Essence of Compiling with Continuations. InProgramming Language Design and Implementation, pages 237-247, 1993.","DOI":"10.1145\/173262.155113"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/pado\/01\/gustavsson\/constr","doi-asserted-by":"crossref","unstructured":"J\u00f6rgen Gustavsson and Josef Svenningsson. Constraint Abstractions. InPrograms as Data Objects, pages 63-83, 2001.","DOI":"10.1007\/3-540-44978-7_5"},{"key":"10.2168\/LMCS-7(2:3)2011_diss\/cmu\/92\/heintze","unstructured":"Nevin Heintze.Set-based program analysis. PhD thesis, Carnegie-Mellon Univ., 1992."},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/paste\/01\/hind\/survey","doi-asserted-by":"crossref","unstructured":"Michael Hind. Pointer analysis: haven't we solved this problem yet? InProgram Analysis For Software Tools and Engineering, pages 54-61, 2001.","DOI":"10.1145\/379605.379665"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/popl\/09\/kobayashi\/hors","doi-asserted-by":"crossref","unstructured":"Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. InPrinciples of Programming Languages, pages 416-428, 2009.","DOI":"10.1145\/1594834.1480933"},{"key":"10.2168\/LMCS-7(2:3)2011_diss\/yale\/88\/kranz","unstructured":"David Kranz.ORBIT: An Optimizing Compiler for Scheme. PhD thesis, Yale University, 1988."},{"issue":"1-2","key":"10.2168\/LMCS-7(2:3)2011_journal\/tcs\/00\/melski\/cflReachab","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0304-3975(00)00049-9","volume":"248","author":"David Melski and Thomas Reps","year":"2000","journal-title":"Theoretical Comp. Sci."},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/icfp\/09\/midtgaard\/directCallRet","doi-asserted-by":"crossref","unstructured":"Jan Midtgaard and Thomas Jensen. Control-flow analysis of function calls and returns by abstract interpretation. InInternational Conference on Functional Programming, pages 287-298, 2009.","DOI":"10.1145\/1631687.1596592"},{"key":"10.2168\/LMCS-7(2:3)2011_diss\/07\/might\/dcfa","unstructured":"Matthew Might.Environment Analysis of Higher-Order Languages. PhD thesis, Georgia Institute of Technology, 2007."},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/icfp\/06\/might\/gcfa","doi-asserted-by":"crossref","unstructured":"Matthew Might and Olin Shivers. Improving Flow Analyses viaGammaCFA: Abstract Garbage Collection and Counting. InInternational Conference on Functional Programming, pages 13-25, 2006.","DOI":"10.1145\/1160074.1159807"},{"key":"10.2168\/LMCS-7(2:3)2011_diss\/diku\/96\/mossin","unstructured":"Christian Mossin.Flow Analysis of Typed Higher-Order Programs. PhD thesis, DIKU, Department of Computer Science, University of Copenhagen, 1996."},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/popl\/01\/rehof\/typeflow","doi-asserted-by":"crossref","unstructured":"Jakob Rehof and Manuel F\u00e4hndrich. Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability. InPrinciples of Programming Languages, pages 54-66, 2001.","DOI":"10.1145\/373243.360208"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/popl\/95\/reps\/interproc","doi-asserted-by":"crossref","unstructured":"Thomas W. Reps, Susan Horwitz, and Shmuel Sagiv. Precise Interprocedural Dataflow Analysis via Graph Reachability. InPrinciples of Programming Languages, pages 49-61, 1995.","DOI":"10.1145\/199448.199462"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/lfp\/92\/sabry\/cps","doi-asserted-by":"crossref","unstructured":"Amr Sabry and Matthias Felleisen. Reasoning About Programs in Continuation-Passing Style. InLISP and Functional Programming, pages 288-298, 1992.","DOI":"10.1145\/141478.141563"},{"key":"10.2168\/LMCS-7(2:3)2011_book\/flowanalysis\/81\/sharir\/interproc","unstructured":"Micha Sharir and Amir Pnueli. Two Approaches to Interprocedural Data Flow Analysis. InProgram Flow Analysis, Theory and Application. Prentice Hall, 1981."},{"key":"10.2168\/LMCS-7(2:3)2011_diss\/cmu\/91\/olin","unstructured":"Olin Shivers.Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie-Mellon University, 1991."},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/pldi\/88\/shivers\/cfaretro","doi-asserted-by":"crossref","unstructured":"Olin Shivers. Higher-Order Control-Flow Analysis in Retrospect: Lessons Learned, Lessons Abandoned. InBest of PLDI, pages 257-269, 2004.","DOI":"10.1145\/989393.989421"},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/pldi\/06\/sridharan\/pointsTo","doi-asserted-by":"crossref","unstructured":"Manu Sridharan and Rastislav Bod\u00edk. Refinement-based context-sensitive points-to analysis for Java. InProgramming Language Design and Implementation, pages 387-400, 2006.","DOI":"10.1145\/1133255.1134027"},{"key":"10.2168\/LMCS-7(2:3)2011_masters\/mit\/78\/steel\/rabbit","unstructured":"Guy L. Steele. Rabbit: A Compiler for Scheme. Master's thesis, MIT, 1978."},{"key":"10.2168\/LMCS-7(2:3)2011_conf\/icfp\/08\/vanhorn\/kcfa","doi-asserted-by":"crossref","unstructured":"David Van Horn and Harry G. Mairson. Decidingk-CFA is complete for EXPTIME. InInternational Conference on Functional Programming, pages 275-282, 2008.","DOI":"10.1145\/1411203.1411243"},{"issue":"1","key":"10.2168\/LMCS-7(2:3)2011_journal\/toplas\/98\/wright\/polysplit","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1145\/271510.271523","volume":"20","author":"Andrew Wright and Suresh Jagannathan","year":"1998","journal-title":"Transactions on Programming Languages and Systems 20(1):166-207, 1998"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/684\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/684\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T21:26:17Z","timestamp":1741728377000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/684"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,1]]},"references-count":31,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(2:3)2011","relation":{"references":[{"id-type":"doi","id":"10.1145\/271510.271523","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1102.3676","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1102.3676","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,5,1]]},"article-number":"684"}}