{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,22]],"date-time":"2026-03-22T08:23:52Z","timestamp":1774167832465,"version":"3.50.1"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"US Air Force Research Lab","award":["FA8750-20-C-0208"],"award-info":[{"award-number":["FA8750-20-C-0208"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>We develop the first theory of control-flow graphs from first principles, and use it to create an algorithm for automatically synthesizing many variants of control-flow graph generators from a language\u2019s operational semantics. Our approach first introduces a new algorithm for converting a large class of small-step operational semantics to an abstract machine. It next uses a technique called \u201dabstract rewriting\u201d to automatically abstract the semantics of a language, which is used both to directly generate a CFG from a program (\u201dinterpreted mode\u201d) and to generate standalone code, similar to a human-written CFG generator, for any program in a language. We show how the choice of two abstraction and projection parameters allow our approach to synthesize several families of CFG-generators useful for different kinds of tools. We prove the correspondence between the generated graphs and the original semantics. We provide and prove an algorithm for automatically proving the termination of interpreted-mode generators. In addition to our theoretical results, we have implemented this algorithm in a tool called Mandate, and show that it produces human-readable code on two medium-size languages with 60\u221280 rules, featuring nearly all intraprocedural control constructs common in modern languages. We then show these CFG-generators were sufficient to build two static analyses atop them. Our work is a promising step towards the grand vision of being able to synthesize all desired tools from the semantics of a programming language.<\/jats:p>","DOI":"10.1145\/3547648","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"742-771","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Automatically deriving control-flow graph generators from operational semantics"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3948-6904","authenticated-orcid":false,"given":"James","family":"Koppel","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0325-1836","authenticated-orcid":false,"given":"Jackson","family":"Kearl","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7604-8252","authenticated-orcid":false,"given":"Armando","family":"Solar-Lezama","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v11i20.21845"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888254"},{"key":"e_1_2_1_3_1","volume-title":"Modern Compiler Implementation in ML","author":"Appel Andrew W.","unstructured":"Andrew W. Appel . 1998. Modern Compiler Implementation in ML . Cambridge University Press . isbn:0-521-58274-1 Andrew W. Appel. 1998. Modern Compiler Implementation in ML. Cambridge University Press. isbn:0-521-58274-1"},{"key":"e_1_2_1_4_1","volume-title":"Term Rewriting and All That","author":"Baader Franz","unstructured":"Franz Baader and Tobias Nipkow . 1999. Term Rewriting and All That . Cambridge University Press . Franz Baader and Tobias Nipkow. 1999. Term Rewriting and All That. Cambridge University Press."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 1995 International Symposium","author":"Bert Didier","year":"1995","unstructured":"Didier Bert and Rachid Echahed . 1995 . Abstraction of Conditional Term Rewriting Systems. In Logic Programming , Proceedings of the 1995 International Symposium , Portland, Oregon, USA , December 4-7, 1995. 162\u2013176. http:\/\/ieeexplore.ieee.org\/xpl\/articleDetails.jsp?arnumber=6300583 Didier Bert and Rachid Echahed. 1995. Abstraction of Conditional Term Rewriting Systems. In Logic Programming, Proceedings of the 1995 International Symposium, Portland, Oregon, USA, December 4-7, 1995. 162\u2013176. http:\/\/ieeexplore.ieee.org\/xpl\/articleDetails.jsp?arnumber=6300583"},{"key":"e_1_2_1_6_1","volume-title":"Abstract Rewriting. In International Workshop on Static Analysis. 178\u2013192","author":"Bert Didier","year":"1993","unstructured":"Didier Bert , Rachid Echahed , and Bjarte M \u00d8 stvold. 1993 . Abstract Rewriting. In International Workshop on Static Analysis. 178\u2013192 . Didier Bert, Rachid Echahed, and Bjarte M \u00d8 stvold. 1993. Abstract Rewriting. In International Workshop on Static Analysis. 178\u2013192."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290357"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676982"},{"key":"e_1_2_1_10_1","unstructured":"Michael Carbin and Armando Solar-Lezama. 2018. MITScript Language Specification. http:\/\/6.s081.scripts.mit.edu\/sp18\/handout-pdfs\/specification.pdf \t\t\t\t  Michael Carbin and Armando Solar-Lezama. 2018. MITScript Language Specification. http:\/\/6.s081.scripts.mit.edu\/sp18\/handout-pdfs\/specification.pdf"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837632"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Cimini Matteo","year":"2017","unstructured":"Matteo Cimini and Jeremy G. Siek . 2017. Automatically Generating the Dynamic Semantics of Gradually Typed Languages . In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 , Paris, France , January 18-20, 2017 . 789\u2013803. http:\/\/dl.acm.org\/citation.cfm?id=3009863 Matteo Cimini and Jeremy G. Siek. 2017. Automatically Generating the Dynamic Semantics of Gradually Typed Languages. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 789\u2013803. http:\/\/dl.acm.org\/citation.cfm?id=3009863"},{"key":"e_1_2_1_13_1","unstructured":"Clifford Noel Click. 1995. Combining Analyses Combining Optimizations. Ph.D. Dissertation. Rice University. \t\t\t\t  Clifford Noel Click. 1995. Combining Analyses Combining Optimizations. Ph.D. Dissertation. Rice University."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158703"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the Eigth International Conference","author":"Codish Michael","year":"1991","unstructured":"Michael Codish , Moreno Falaschi , and Kim Marriott . 1991 . Suspension Analysis for Concurrent Logic Programs. In Logic Programming , Proceedings of the Eigth International Conference , Paris, France , June 24-28, 1991. 331\u2013345. Michael Codish, Moreno Falaschi, and Kim Marriott. 1991. Suspension Analysis for Concurrent Logic Programs. In Logic Programming, Proceedings of the Eigth International Conference, Paris, France, June 24-28, 1991. 331\u2013345."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411206"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2009.10.004"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.02.023"},{"key":"e_1_2_1_20_1","volume-title":"Refocusing in Reduction Semantics. BRICS Report Series, 11, 26","author":"Danvy Olivier","year":"2004","unstructured":"Olivier Danvy and Lasse R Nielsen . 2004. Refocusing in Reduction Semantics. BRICS Report Series, 11, 26 ( 2004 ). Olivier Danvy and Lasse R Nielsen. 2004. Refocusing in Reduction Semantics. BRICS Report Series, 11, 26 (2004)."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110256"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814308"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80022-6"},{"key":"e_1_2_1_24_1","volume-title":"Robert Bruce Findler, and Matthew Flatt","author":"Felleisen Matthias","year":"2009","unstructured":"Matthias Felleisen , Robert Bruce Findler, and Matthew Flatt . 2009 . Semantics Engineering with PLT Redex. Mit Press . Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. Mit Press."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661088.2661098"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500604"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001559"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_2_1_31_1","volume-title":"Concurrency, Compositionality, and Correctness","author":"Huizing Cornelis","unstructured":"Cornelis Huizing , Ron Koymans , and Ruurd Kuiper . 2010. A Small Step for Mankind . In Concurrency, Compositionality, and Correctness . Springer , 66\u201373. Cornelis Huizing, Ron Koymans, and Ruurd Kuiper. 2010. A Small Step for Mankind. In Concurrency, Compositionality, and Correctness. Springer, 66\u201373."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA087640"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80692-9"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199536"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Neil D Jones. 1981. Flow Analysis of Lambda Expressions. In International Colloquium on Automata Languages and Programming. 114\u2013128. \t\t\t\t  Neil D Jones. 1981. Flow Analysis of Lambda Expressions. In International Colloquium on Automata Languages and Programming. 114\u2013128.","DOI":"10.1007\/3-540-10843-2_10"},{"key":"e_1_2_1_36_1","unstructured":"Jasper FT Kamperman and Humphrey Robert Walters. 1993. ARM Abstract Rewriting Machine. \t\t\t\t  Jasper FT Kamperman and Humphrey Robert Walters. 1993. ARM Abstract Rewriting Machine."},{"key":"e_1_2_1_37_1","unstructured":"Andy King and Mark Longley. 1995. Abstract Matching Can Improve on Abstract Unification. \t\t\t\t  Andy King and Mark Longley. 1995. Abstract Matching Can Improve on Abstract Unification."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103691"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276492"},{"key":"e_1_2_1_40_1","volume-title":"Symposium on Trends in Functional Programming.","author":"Lakin Matthew R","year":"2007","unstructured":"Matthew R Lakin and Andrew M Pitts . 2007 . A Metalanguage for Structural Operational Semantics . In Symposium on Trends in Functional Programming. Matthew R Lakin and Andrew M Pitts. 2007. A Metalanguage for Structural Operational Semantics. In Symposium on Trends in Functional Programming."},{"key":"e_1_2_1_41_1","unstructured":"Dallas S Lankford. 1975. Canonical Inference. University of Texas Department of Mathematics and Computer Sciences. \t\t\t\t  Dallas S Lankford. 1975. Canonical Inference. University of Texas Department of Mathematics and Computer Sciences."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3135932.3135941"},{"key":"e_1_2_1_43_1","unstructured":"Panagiotis Manolios. 2001. Mechanical Verification of Reactive Systems. \t\t\t\t  Panagiotis Manolios. 2001. Mechanical Verification of Reactive Systems."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187672"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_23"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596592"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628143"},{"key":"e_1_2_1_48_1","volume-title":"Principles of Program Analysis","author":"Nielson Flemming","unstructured":"Flemming Nielson , Hanne R Nielson , and Chris Hankin . 2015. Principles of Program Analysis . Springer . Flemming Nielson, Hanne R Nielson, and Chris Hankin. 2015. Principles of Program Analysis. Springer."},{"key":"e_1_2_1_49_1","volume-title":"Polyglot: An Extensible Compiler Framework for Java. In International Conference on Compiler Construction. 138\u2013152","author":"Nystrom Nathaniel","year":"2003","unstructured":"Nathaniel Nystrom , Michael R Clarkson , and Andrew C Myers . 2003 . Polyglot: An Extensible Compiler Framework for Java. In International Conference on Compiler Construction. 138\u2013152 . Nathaniel Nystrom, Michael R Clarkson, and Andrew C Myers. 2003. Polyglot: An Extensible Compiler Framework for Java. In International Conference on Compiler Construction. 138\u2013152."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737991"},{"key":"e_1_2_1_51_1","volume-title":"Concrete Model Checking with Abstract Matching and Refinement. In International Conference on Computer Aided Verification. 52\u201366","author":"P\u0103s\u0103reanu Corina S","year":"2005","unstructured":"Corina S P\u0103s\u0103reanu , Radek Pel\u00e1nek , and Willem Visser . 2005 . Concrete Model Checking with Abstract Matching and Refinement. In International Conference on Computer Aided Verification. 52\u201366 . Corina S P\u0103s\u0103reanu, Radek Pel\u00e1nek, and Willem Visser. 2005. Concrete Model Checking with Abstract Matching and Refinement. In International Conference on Computer Aided Verification. 52\u201366."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192398"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110288"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_15"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.10.001"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_2_1_57_1","volume-title":"Abstract Interpretation of Small-Step Semantics. In LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages. 76\u201399","author":"Schmidt David A","year":"1996","unstructured":"David A Schmidt . 1996 . Abstract Interpretation of Small-Step Semantics. In LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages. 76\u201399 . David A Schmidt. 1996. Abstract Interpretation of Small-Step Semantics. In LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages. 76\u201399."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1988783.1988785"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491979"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970298"},{"key":"e_1_2_1_62_1","volume-title":"Abstracting Abstract Machines. In 15th ACM SIGPLAN International Conference on Functional Programming, ICFP\u201910","author":"Horn David Van","year":"2010","unstructured":"David Van Horn and Matthew Might . 2010 . Abstracting Abstract Machines. In 15th ACM SIGPLAN International Conference on Functional Programming, ICFP\u201910 . David Van Horn and Matthew Might. 2010. Abstracting Abstract Machines. In 15th ACM SIGPLAN International Conference on Functional Programming, ICFP\u201910."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_8"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236800"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014408032446"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547648","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547648","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547648"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":63,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547648"],"URL":"https:\/\/doi.org\/10.1145\/3547648","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}