{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T17:55:43Z","timestamp":1759341343782,"version":"3.41.0"},"reference-count":79,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2021,1,20]],"date-time":"2021-01-20T00:00:00Z","timestamp":1611100800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004836","name":"Danish Council for Independent Research","doi-asserted-by":"crossref","award":["\u00a00602-02327B"],"award-info":[{"award-number":["\u00a00602-02327B"]}],"id":[{"id":"10.13039\/501100004836","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100012774","name":"Innovation Fund Denmark","doi-asserted-by":"crossref","award":["\u00a07039-00072B"],"award-info":[{"award-number":["\u00a07039-00072B"]}],"id":[{"id":"10.13039\/100012774","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2021,1,31]]},"abstract":"<jats:p>High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backtracking, and generalized iterators. We present the design and implementation of an abstract interpretation tool, Rabit, for verifying inductive type and shape properties for transformations written in such languages. We describe how to perform abstract interpretation based on operational semantics, specifically focusing on the challenges arising when analyzing the expressive traversals and pattern matching. Finally, we evaluate Rabit on a series of transformations (normalization, desugaring, refactoring, code generators, type inference, etc.) showing that we can effectively verify stated properties.<\/jats:p>","DOI":"10.1145\/3409805","type":"journal-article","created":{"date-parts":[[2021,1,20]],"date-time":"2021-01-20T19:18:06Z","timestamp":1611170286000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Verification of Program Transformations with Inductive Refinement Types"],"prefix":"10.1145","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3445-2334","authenticated-orcid":false,"given":"Ahmad Salim","family":"Al-Sibahi","sequence":"first","affiliation":[{"name":"University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas P.","family":"Jensen","sequence":"additional","affiliation":[{"name":"INRIA Rennes, France and University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aleksandar S.","family":"Dimovski","sequence":"additional","affiliation":[{"name":"Mother Teresa University, Skopje, Macedonia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej","family":"W\u0105sowski","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,20]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Murphy","author":"Aiken Alexander","year":"1991","unstructured":"Alexander Aiken and Brian R . Murphy . 1991 . Implementing regular tree expressions. In FPLCA\u2019 91. 427--447. https:\/\/doi.org\/10.1007\/3540543961_21 10.1007\/3540543961_21 Alexander Aiken and Brian R. Murphy. 1991. Implementing regular tree expressions. In FPLCA\u201991. 427--447. https:\/\/doi.org\/10.1007\/3540543961_21"},{"key":"e_1_2_1_2_1","unstructured":"Ahmad Salim Al-Sibahi. 2017. The formal semantics of rascal light. CoRR abs\/1703.02312. Retrieved from http:\/\/arxiv.org\/abs\/1703.02312.  Ahmad Salim Al-Sibahi. 2017. The formal semantics of rascal light. CoRR abs\/1703.02312. Retrieved from http:\/\/arxiv.org\/abs\/1703.02312."},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Ahmad Salim Al-Sibahi Aleksandar S. Dimovski and Andrzej Wasowski. 2016. Symbolic execution of high-level transformations. In SLE\u201916. 207--220.  Ahmad Salim Al-Sibahi Aleksandar S. Dimovski and Andrzej Wasowski. 2016. Symbolic execution of high-level transformations. In SLE\u201916. 207--220.","DOI":"10.1145\/2997364.2997382"},{"key":"e_1_2_1_4_1","volume-title":"Rasmus Ejlers M\u00f8gelberg, and Andrzej W\u0105sowski","author":"Al-Sibahi Ahmad Salim","year":"2020","unstructured":"Ahmad Salim Al-Sibahi , Thomas Jensen , Rasmus Ejlers M\u00f8gelberg, and Andrzej W\u0105sowski . 2020 . Galois Connections for Recursive Types. Springer International Publishing , Cham, 105--131. DOI:https:\/\/doi.org\/10.1007\/978-3-030-41103-9_4 10.1007\/978-3-030-41103-9_4 Ahmad Salim Al-Sibahi, Thomas Jensen, Rasmus Ejlers M\u00f8gelberg, and Andrzej W\u0105sowski. 2020. Galois Connections for Recursive Types. Springer International Publishing, Cham, 105--131. DOI:https:\/\/doi.org\/10.1007\/978-3-030-41103-9_4"},{"key":"#cr-split#-e_1_2_1_5_1.1","doi-asserted-by":"crossref","unstructured":"Ahmad Salim Al-Sibahi Thomas P. Jensen Aleksandar S. Dimovski and Andrzej Wasowski. 2018. Verification of high-level transformations with inductive refinement types. In GPCE'18 Eric Van Wyk and Tiark Rompf (Eds.). ACM 147--160. DOI:https:\/\/doi.org\/10.1145\/3278122.3278125 10.1145\/3278122.3278125","DOI":"10.1145\/3278122.3278125"},{"key":"#cr-split#-e_1_2_1_5_1.2","doi-asserted-by":"crossref","unstructured":"Ahmad Salim Al-Sibahi Thomas P. Jensen Aleksandar S. Dimovski and Andrzej Wasowski. 2018. Verification of high-level transformations with inductive refinement types. In GPCE'18 Eric Van Wyk and Tiark Rompf (Eds.). ACM 147--160. DOI:https:\/\/doi.org\/10.1145\/3278122.3278125","DOI":"10.1145\/3393934.3278125"},{"key":"#cr-split#-e_1_2_1_6_1.1","doi-asserted-by":"crossref","unstructured":"Aws Albarghouthi Josh Berdine Byron Cook and Zachary Kincaid. 2015. Spatial interpolants. In ESOP'15. 634--660. DOI:https:\/\/doi.org\/10.1007\/978-3-662-46669-8_26 10.1007\/978-3-662-46669-8_26","DOI":"10.1007\/978-3-662-46669-8_26"},{"key":"#cr-split#-e_1_2_1_6_1.2","doi-asserted-by":"crossref","unstructured":"Aws Albarghouthi Josh Berdine Byron Cook and Zachary Kincaid. 2015. Spatial interpolants. In ESOP'15. 634--660. DOI:https:\/\/doi.org\/10.1007\/978-3-662-46669-8_26","DOI":"10.1007\/978-3-662-46669-8_26"},{"key":"#cr-split#-e_1_2_1_7_1.1","doi-asserted-by":"crossref","unstructured":"Oana Fabiana Andreescu Thomas Jensen and St\u00e9phane Lescuyer. 2015. Dependency analysis of functional specifications with algebraic data structures. In ICFEM'15. 116--133. DOI:https:\/\/doi.org\/10.1007\/978-3-319-25423-4_8 10.1007\/978-3-319-25423-4_8","DOI":"10.1007\/978-3-319-25423-4_8"},{"key":"#cr-split#-e_1_2_1_7_1.2","doi-asserted-by":"crossref","unstructured":"Oana Fabiana Andreescu Thomas Jensen and St\u00e9phane Lescuyer. 2015. Dependency analysis of functional specifications with algebraic data structures. In ICFEM'15. 116--133. DOI:https:\/\/doi.org\/10.1007\/978-3-319-25423-4_8","DOI":"10.1007\/978-3-319-25423-4_8"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.11.003"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/985799.985801"},{"key":"#cr-split#-e_1_2_1_10_1.1","doi-asserted-by":"crossref","unstructured":"V\u00e9ronique Benzaken Giuseppe Castagna Kim Nguyen and J\u00e9r\u00f4me Sim\u00e9on. 2013. Static and dynamic semantics of NoSQL languages. In POPL'13. 101--114. DOI:https:\/\/doi.org\/10.1145\/2429069.2429083 10.1145\/2429069.2429083","DOI":"10.1145\/2480359.2429083"},{"key":"#cr-split#-e_1_2_1_10_1.2","doi-asserted-by":"crossref","unstructured":"V\u00e9ronique Benzaken Giuseppe Castagna Kim Nguyen and J\u00e9r\u00f4me Sim\u00e9on. 2013. Static and dynamic semantics of NoSQL languages. In POPL'13. 101--114. DOI:https:\/\/doi.org\/10.1145\/2429069.2429083","DOI":"10.1145\/2480359.2429083"},{"key":"#cr-split#-e_1_2_1_11_1.1","doi-asserted-by":"crossref","unstructured":"Martin Bodin Thomas Jensen and Alan Schmitt. 2015. Certified abstract interpretation with pretty-big-step semantics. In CPP'15. 29--40. DOI:https:\/\/doi.org\/10.1145\/2676724.2693174 10.1145\/2676724.2693174","DOI":"10.1145\/2676724.2693174"},{"key":"#cr-split#-e_1_2_1_11_1.2","doi-asserted-by":"crossref","unstructured":"Martin Bodin Thomas Jensen and Alan Schmitt. 2015. Certified abstract interpretation with pretty-big-step semantics. In CPP'15. 29--40. DOI:https:\/\/doi.org\/10.1145\/2676724.2693174","DOI":"10.1145\/2676724.2693174"},{"key":"#cr-split#-e_1_2_1_12_1.1","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani Cezara Dragoi Constantin Enea and Mihaela Sighireanu. 2012. Abstract domains for automated reasoning about list-manipulating programs with infinite data. In VMCAI'12. 1--22. DOI:https:\/\/doi.org\/10.1007\/978-3-642-27940-9_1 10.1007\/978-3-642-27940-9_1","DOI":"10.1007\/978-3-642-27940-9_1"},{"key":"#cr-split#-e_1_2_1_12_1.2","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani Cezara Dragoi Constantin Enea and Mihaela Sighireanu. 2012. Abstract domains for automated reasoning about list-manipulating programs with infinite data. In VMCAI'12. 1--22. DOI:https:\/\/doi.org\/10.1007\/978-3-642-27940-9_1","DOI":"10.1007\/978-3-642-27940-9_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.11.003"},{"key":"#cr-split#-e_1_2_1_14_1.1","doi-asserted-by":"crossref","unstructured":"Giuseppe Castagna and Kim Nguyen. 2008. Typed iterators for XML. In ICFP'08. 15--26. DOI:https:\/\/doi.org\/10.1145\/1411204.1411210 10.1145\/1411204.1411210","DOI":"10.1145\/1411203.1411210"},{"key":"#cr-split#-e_1_2_1_14_1.2","doi-asserted-by":"crossref","unstructured":"Giuseppe Castagna and Kim Nguyen. 2008. Typed iterators for XML. In ICFP'08. 15--26. DOI:https:\/\/doi.org\/10.1145\/1411204.1411210","DOI":"10.1145\/1411203.1411210"},{"key":"#cr-split#-e_1_2_1_15_1.1","doi-asserted-by":"crossref","unstructured":"Bor-Yuh Evan Chang and Xavier Rival. 2008. Relational inductive shape analysis. In POPL'08. 247--260. DOI:https:\/\/doi.org\/10.1145\/1328438.1328469 10.1145\/1328438.1328469","DOI":"10.1145\/1328438.1328469"},{"key":"#cr-split#-e_1_2_1_15_1.2","doi-asserted-by":"crossref","unstructured":"Bor-Yuh Evan Chang and Xavier Rival. 2008. Relational inductive shape analysis. In POPL'08. 247--260. DOI:https:\/\/doi.org\/10.1145\/1328438.1328469","DOI":"10.1145\/1328897.1328469"},{"key":"#cr-split#-e_1_2_1_16_1.1","doi-asserted-by":"crossref","unstructured":"James Chapman Pierre-\u00c9variste Dagand Conor McBride and Peter Morris. 2010. The gentle art of levitation. In ICFP'10. 3--14. DOI:https:\/\/doi.org\/10.1145\/1863543.1863547 10.1145\/1863543.1863547","DOI":"10.1145\/1863543.1863547"},{"key":"#cr-split#-e_1_2_1_16_1.2","doi-asserted-by":"crossref","unstructured":"James Chapman Pierre-\u00c9variste Dagand Conor McBride and Peter Morris. 2010. The gentle art of levitation. In ICFP'10. 3--14. DOI:https:\/\/doi.org\/10.1145\/1863543.1863547","DOI":"10.1145\/1932681.1863547"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.04.002"},{"volume-title":"Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. 243--268. DOI:https:\/\/doi.org\/10.1007\/978-3-540-39910-0_11","author":"Cousot Patrick","key":"e_1_2_1_18_1","unstructured":"Patrick Cousot . 2003. Verification by abstract interpretation . In Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. 243--268. DOI:https:\/\/doi.org\/10.1007\/978-3-540-39910-0_11 10.1007\/978-3-540-39910-0_11 Patrick Cousot. 2003. Verification by abstract interpretation. In Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. 243--268. DOI:https:\/\/doi.org\/10.1007\/978-3-540-39910-0_11"},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. 1995. Formal language grammar and set-constraint-based program analysis by abstract interpretation. In FPCA\u201995. 170--181. http:\/\/doi.acm.org\/10.1145\/224164.224199  Patrick Cousot and Radhia Cousot. 1995. Formal language grammar and set-constraint-based program analysis by abstract interpretation. In FPCA\u201995. 170--181. http:\/\/doi.acm.org\/10.1145\/224164.224199","DOI":"10.1145\/224164.224199"},{"key":"#cr-split#-e_1_2_1_20_1.1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. 2002. Modular static program analysis. In CC'02. 159--178. DOI:https:\/\/doi.org\/10.1007\/3-540-45937-5_13 10.1007\/3-540-45937-5_13","DOI":"10.1007\/3-540-45937-5_13"},{"key":"#cr-split#-e_1_2_1_20_1.2","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. 2002. Modular static program analysis. In CC'02. 159--178. DOI:https:\/\/doi.org\/10.1007\/3-540-45937-5_13","DOI":"10.1007\/3-540-45937-5_13"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2635137"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110256"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.05.017"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/359138.359142"},{"volume-title":"Refactoring\u2014Improving the Design of Existing Code","author":"Fowler Martin","key":"e_1_2_1_25_1","unstructured":"Martin Fowler . 1999. Refactoring\u2014Improving the Design of Existing Code . Addison-Wesley . Martin Fowler. 1999. Refactoring\u2014Improving the Design of Existing Code. Addison-Wesley."},{"key":"e_1_2_1_26_1","volume-title":"Freeman and Frank Pfenning","author":"Timothy","year":"1991","unstructured":"Timothy S. Freeman and Frank Pfenning . 1991 . Refinement types for ML. In PLDI\u2019 91. 268--277. http:\/\/doi.acm.org\/10.1145\/113445.113468 Timothy S. Freeman and Frank Pfenning. 1991. Refinement types for ML. In PLDI\u201991. 268--277. http:\/\/doi.acm.org\/10.1145\/113445.113468"},{"key":"e_1_2_1_27_1","volume-title":"ML Workshop","volume":"13","author":"Garrigue Jacques","year":"1998","unstructured":"Jacques Garrigue . 1998 . Programming with polymorphic variants . In ML Workshop , Vol. 13 . Jacques Garrigue. 1998. Programming with polymorphic variants. In ML Workshop, Vol. 13."},{"key":"e_1_2_1_28_1","volume-title":"JSSST Workshop on Programming and Programming Languages.","author":"Garrigue Jacques","year":"2004","unstructured":"Jacques Garrigue . 2004 . Typing deep pattern-matching in presence of polymorphic variants . In JSSST Workshop on Programming and Programming Languages. Jacques Garrigue. 2004. Typing deep pattern-matching in presence of polymorphic variants. In JSSST Workshop on Programming and Programming Languages."},{"key":"#cr-split#-e_1_2_1_29_1.1","doi-asserted-by":"crossref","unstructured":"Nicolas Halbwachs and Mathias P\u00e9ron. 2008. Discovering properties about arrays in simple programs. In PLDI'08. 339--348. DOI:https:\/\/doi.org\/10.1145\/1375581.1375623 10.1145\/1375581.1375623","DOI":"10.1145\/1379022.1375623"},{"key":"#cr-split#-e_1_2_1_29_1.2","doi-asserted-by":"crossref","unstructured":"Nicolas Halbwachs and Mathias P\u00e9ron. 2008. Discovering properties about arrays in simple programs. In PLDI'08. 339--348. DOI:https:\/\/doi.org\/10.1145\/1375581.1375623","DOI":"10.1145\/1379022.1375623"},{"volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"Harrison John","key":"e_1_2_1_30_1","unstructured":"John Harrison . 2009. Handbook of Practical Logic and Automated Reasoning . Cambridge University Press . John Harrison. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press."},{"key":"#cr-split#-e_1_2_1_31_1.1","doi-asserted-by":"crossref","unstructured":"David Van Horn and Matthew Might. 2010. Abstracting abstract machines. In ICFP'10 Paul Hudak and Stephanie Weirich (Eds.). ACM 51--62. DOI:https:\/\/doi.org\/10.1145\/1863543.1863553 10.1145\/1863543.1863553","DOI":"10.1145\/1863543.1863553"},{"key":"#cr-split#-e_1_2_1_31_1.2","doi-asserted-by":"crossref","unstructured":"David Van Horn and Matthew Might. 2010. Abstracting abstract machines. In ICFP'10 Paul Hudak and Stephanie Weirich (Eds.). ACM 51--62. DOI:https:\/\/doi.org\/10.1145\/1863543.1863553","DOI":"10.1145\/1932681.1863553"},{"key":"e_1_2_1_32_1","volume-title":"Aleksandar S. Dimovski, Juha Erik Savolainen, Krzysztof Sierszecki, and Andrzej W\u0105sowski.","author":"Iosif-Laz\u0103r Alexandru Florin","year":"2015","unstructured":"Alexandru Florin Iosif-Laz\u0103r , Ahmad Salim Al-Sibahi , Aleksandar S. Dimovski, Juha Erik Savolainen, Krzysztof Sierszecki, and Andrzej W\u0105sowski. 2015 . Experiences from designing and validating a software modernization transformation (E). In ASE\u2019 15. 597--607. DOI:https:\/\/doi.org\/10.1109\/ASE.2015.84 10.1109\/ASE.2015.84 Alexandru Florin Iosif-Laz\u0103r, Ahmad Salim Al-Sibahi, Aleksandar S. Dimovski, Juha Erik Savolainen, Krzysztof Sierszecki, and Andrzej W\u0105sowski. 2015. Experiences from designing and validating a software modernization transformation (E). In ASE\u201915. 597--607. DOI:https:\/\/doi.org\/10.1109\/ASE.2015.84"},{"volume-title":"GADTs meet their match: Pattern-matching warnings that account for GADTs, guards, and laziness. In ICFP\u201915","author":"Karachalias Georgios","key":"e_1_2_1_33_1","unstructured":"Georgios Karachalias , Tom Schrijvers , Dimitrios Vytiniotis , and Simon L . Peyton Jones. 2015 . GADTs meet their match: Pattern-matching warnings that account for GADTs, guards, and laziness. In ICFP\u201915 , Kathleen Fisher and John H. Reppy (Eds.). ACM, 424--436. DOI:https:\/\/doi.org\/10.1145\/2784731.2784748 10.1145\/2784731.2784748 Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2015. GADTs meet their match: Pattern-matching warnings that account for GADTs, guards, and laziness. In ICFP\u201915, Kathleen Fisher and John H. Reppy (Eds.). ACM, 424--436. DOI:https:\/\/doi.org\/10.1145\/2784731.2784748"},{"key":"e_1_2_1_34_1","series-title":"Lecture Notes in Computer Science","volume-title":"VMCAI\u201920","author":"Keidel Sven","unstructured":"Sven Keidel and Sebastian Erdweg . 2020. A systematic approach to abstract interpretation of program transformations . In VMCAI\u201920 , Lecture Notes in Computer Science , Dirk Beyer and Damien Zufferey (Eds.), Vol. 11990 . Springer , 136--157. DOI:https:\/\/doi.org\/10.1007\/978-3-030-39322-9_7 10.1007\/978-3-030-39322-9_7 Sven Keidel and Sebastian Erdweg. 2020. A systematic approach to abstract interpretation of program transformations. In VMCAI\u201920, Lecture Notes in Computer Science, Dirk Beyer and Damien Zufferey (Eds.), Vol. 11990. Springer, 136--157. DOI:https:\/\/doi.org\/10.1007\/978-3-030-39322-9_7"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230624"},{"key":"#cr-split#-e_1_2_1_36_1.1","doi-asserted-by":"crossref","unstructured":"Paul Klint Tijs van der Storm and Jurgen Vinju. 2011. EASY meta-programming with Rascal. In GTTSE III Jo\u00e3oM. Fernandes Ralf L\u00e4mmel Joost Visser and Jo\u00e3o Saraiva (Eds.). 222--289. DOI:https:\/\/doi.org\/10.1007\/978-3-642-18023-1_6 10.1007\/978-3-642-18023-1_6","DOI":"10.1007\/978-3-642-18023-1_6"},{"key":"#cr-split#-e_1_2_1_36_1.2","doi-asserted-by":"crossref","unstructured":"Paul Klint Tijs van der Storm and Jurgen Vinju. 2011. EASY meta-programming with Rascal. In GTTSE III Jo\u00e3oM. Fernandes Ralf L\u00e4mmel Joost Visser and Jo\u00e3o Saraiva (Eds.). 222--289. DOI:https:\/\/doi.org\/10.1007\/978-3-642-18023-1_6","DOI":"10.1007\/978-3-642-18023-1_6"},{"key":"e_1_2_1_37_1","volume-title":"Nemytykh","author":"Lisitsa Alexei P.","year":"2015","unstructured":"Alexei P. Lisitsa and Andrei P . Nemytykh . 2015 . Finite countermodel based verification for program transformation (A case study). In VPT@ETAPS\u201915, Alexei Lisitsa, Andrei P. Nemytykh, and Alberto Pettorossi (Eds .), Vol. 199 . 15--32. DOI:https:\/\/doi.org\/10.4204\/EPTCS.199.2 10.4204\/EPTCS.199.2 Alexei P. Lisitsa and Andrei P. Nemytykh. 2015. Finite countermodel based verification for program transformation (A case study). In VPT@ETAPS\u201915, Alexei Lisitsa, Andrei P. Nemytykh, and Alberto Pettorossi (Eds.), Vol. 199. 15--32. DOI:https:\/\/doi.org\/10.4204\/EPTCS.199.2"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2016.01.005"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291201.1291208"},{"key":"e_1_2_1_40_1","volume-title":"Jones","author":"Mycroft Alan","year":"1985","unstructured":"Alan Mycroft and Neil D . Jones . 1985 . A relational framework for abstract interpretation. In Programs as Data Objects . 156--171. DOI:https:\/\/doi.org\/10.1007\/3-540-16446-4_9 10.1007\/3-540-16446-4_9 Alan Mycroft and Neil D. Jones. 1985. A relational framework for abstract interpretation. In Programs as Data Objects. 156--171. DOI:https:\/\/doi.org\/10.1007\/3-540-16446-4_9"},{"key":"#cr-split#-e_1_2_1_41_1.1","doi-asserted-by":"crossref","unstructured":"Valentin Perrelle and Nicolas Halbwachs. 2010. An analysis of permutations in arrays. In VMCAI'10. 279--294. DOI:https:\/\/doi.org\/10.1007\/978-3-642-11319-2_21 10.1007\/978-3-642-11319-2_21","DOI":"10.1007\/978-3-642-11319-2_21"},{"key":"#cr-split#-e_1_2_1_41_1.2","doi-asserted-by":"crossref","unstructured":"Valentin Perrelle and Nicolas Halbwachs. 2010. An analysis of permutations in arrays. In VMCAI'10. 279--294. DOI:https:\/\/doi.org\/10.1007\/978-3-642-11319-2_21","DOI":"10.1007\/978-3-642-11319-2_21"},{"key":"e_1_2_1_42_1","volume-title":"Whalen","author":"Pham Tuan-Hung","year":"2013","unstructured":"Tuan-Hung Pham and Michael W . Whalen . 2013 . An improved unrolling-based decision procedure for algebraic data types. In VSTTE\u2019 13. 129--148. DOI:https:\/\/doi.org\/10.1007\/978-3-642-54108-7_7 10.1007\/978-3-642-54108-7_7 Tuan-Hung Pham and Michael W. Whalen. 2013. An improved unrolling-based decision procedure for algebraic data types. In VSTTE\u201913. 129--148. DOI:https:\/\/doi.org\/10.1007\/978-3-642-54108-7_7"},{"key":"#cr-split#-e_1_2_1_43_1.1","doi-asserted-by":"crossref","unstructured":"Andrew Reynolds and Viktor Kuncak. 2015. Induction for SMT Solvers. In VMCAI'15. 80--98. DOI:https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5 10.1007\/978-3-662-46081-8_5","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"#cr-split#-e_1_2_1_43_1.2","doi-asserted-by":"crossref","unstructured":"Andrew Reynolds and Viktor Kuncak. 2015. Induction for SMT Solvers. In VMCAI'15. 80--98. DOI:https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"#cr-split#-e_1_2_1_45_1.1","doi-asserted-by":"crossref","unstructured":"Xavier Rival Antoine Toubhans and Bor-Yuh Evan Chang. 2014. Construction of abstract domains for heterogeneous properties. In ISoLA'14. 489--492. DOI:https:\/\/doi.org\/10.1007\/978-3-662-45231-8_40 10.1007\/978-3-662-45231-8_40","DOI":"10.1007\/978-3-662-45231-8_40"},{"key":"#cr-split#-e_1_2_1_45_1.2","doi-asserted-by":"crossref","unstructured":"Xavier Rival Antoine Toubhans and Bor-Yuh Evan Chang. 2014. Construction of abstract domains for heterogeneous properties. In ISoLA'14. 489--492. DOI:https:\/\/doi.org\/10.1007\/978-3-662-45231-8_40","DOI":"10.1007\/978-3-662-45231-8_40"},{"key":"#cr-split#-e_1_2_1_46_1.1","doi-asserted-by":"crossref","unstructured":"Mads Rosendahl. 2013. Abstract interpretation as a programming language. In Semantics Abstract Interpretation and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday. 84--104. DOI:https:\/\/doi.org\/10.4204\/EPTCS.129.7 10.4204\/EPTCS.129.7","DOI":"10.4204\/EPTCS.129.0"},{"key":"#cr-split#-e_1_2_1_46_1.2","doi-asserted-by":"crossref","unstructured":"Mads Rosendahl. 2013. Abstract interpretation as a programming language. In Semantics Abstract Interpretation and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday. 84--104. DOI:https:\/\/doi.org\/10.4204\/EPTCS.129.7","DOI":"10.4204\/EPTCS.129.7"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_49_1","volume-title":"Comput","author":"Schmidt David A.","year":"1998","unstructured":"David A. Schmidt . 1998. Trace-based abstract interpretation of operational semantics. Lisp Symbol \u2019 Comput \u2019 10, 3 ( 1998 ), 237--271. David A. Schmidt. 1998. Trace-based abstract interpretation of operational semantics. Lisp Symbol\u2019 Comput\u2019 10, 3 (1998), 237--271."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"volume-title":"Programming Language Concepts","author":"Sestoft Peter","key":"e_1_2_1_51_1","unstructured":"Peter Sestoft and Niels Hallenberg . 2017. Programming Language Concepts . Springer . Peter Sestoft and Niels Hallenberg. 2017. Programming Language Concepts. Springer."},{"key":"e_1_2_1_52_1","unstructured":"Micha Sharir and Amir Pnueli. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. Chapter 7.  Micha Sharir and Amir Pnueli. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. Chapter 7."},{"key":"e_1_2_1_53_1","series-title":"Lecture Notes in Computer Science","volume-title":"Lightweight language processing in kiama","author":"Sloane M.","unstructured":"Anthony M. Sloane . 2011. Lightweight language processing in kiama . In GTTSE III, Jo\u00e3oM. Fernandes, Ralf L\u00e4mmel, Joost Visser, and Jo\u00e3o Saraiva (Eds.). Lecture Notes in Computer Science , Vol. 6491 . Springer , Berlin , 408--425. DOI:https:\/\/doi.org\/10.1007\/978-3-642-18023-1_12 10.1007\/978-3-642-18023-1_12 AnthonyM. Sloane. 2011. Lightweight language processing in kiama. In GTTSE III, Jo\u00e3oM. Fernandes, Ralf L\u00e4mmel, Joost Visser, and Jo\u00e3o Saraiva (Eds.). Lecture Notes in Computer Science, Vol. 6491. Springer, Berlin, 408--425. DOI:https:\/\/doi.org\/10.1007\/978-3-642-18023-1_12"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1137\/0211062"},{"volume-title":"POPL\u201910, Manuel V","author":"Suter Philippe","key":"e_1_2_1_55_1","unstructured":"Philippe Suter , Mirco Dotta , and Viktor Kuncak . 2010. Decision procedures for algebraic data types with abstractions . In POPL\u201910, Manuel V . Hermenegildo and Jens Palsberg (Eds.). ACM , 199--210. DOI:https:\/\/doi.org\/10.1145\/1706299.1706325 10.1145\/1706299.1706325 Philippe Suter, Mirco Dotta, and Viktor Kuncak. 2010. Decision procedures for algebraic data types with abstractions. In POPL\u201910, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 199--210. DOI:https:\/\/doi.org\/10.1145\/1706299.1706325"},{"key":"e_1_2_1_56_1","volume-title":"Bor-Yuh Evan Chang, and Xavier Rival","author":"Toubhans Antoine","year":"2013","unstructured":"Antoine Toubhans , Bor-Yuh Evan Chang, and Xavier Rival . 2013 . Reduced product combination of abstract domains for shapes. In VMCAI\u2019 13. 375--395. DOI:https:\/\/doi.org\/10.1007\/978-3-642-35873-9_23 10.1007\/978-3-642-35873-9_23 Antoine Toubhans, Bor-Yuh Evan Chang, and Xavier Rival. 2013. Reduced product combination of abstract domains for shapes. In VMCAI\u201913. 375--395. DOI:https:\/\/doi.org\/10.1007\/978-3-642-35873-9_23"},{"key":"e_1_2_1_57_1","volume-title":"Patrick Maxim Rondon, and Ranjit Jhala","author":"Vazou Niki","year":"2013","unstructured":"Niki Vazou , Patrick Maxim Rondon, and Ranjit Jhala . 2013 . Abstract refinement types. In ESOP\u2019 13. 209--228. DOI:https:\/\/doi.org\/10.1007\/978-3-642-37036-6_13 10.1007\/978-3-642-37036-6_13 Niki Vazou, Patrick Maxim Rondon, and Ranjit Jhala. 2013. Abstract refinement types. In ESOP\u201913. 209--228. DOI:https:\/\/doi.org\/10.1007\/978-3-642-37036-6_13"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"},{"volume-title":"Information systems","author":"Winskel Glynn","key":"e_1_2_1_59_1","unstructured":"Glynn Winskel . 1993. Information systems . MIT Press , Chapter 12. Glynn Winskel. 1993. Information systems. MIT Press, Chapter 12."},{"key":"e_1_2_1_60_1","unstructured":"Niklaus Wirth. 1996. Compiler Construction. Addison-Wesley.  Niklaus Wirth. 1996. Compiler Construction. Addison-Wesley."},{"key":"#cr-split#-e_1_2_1_61_1.1","doi-asserted-by":"crossref","unstructured":"Hongwei Xi and Frank Pfenning. 1998. Eliminating array bound checking through dependent types. In PLDI'98. 249--257. DOI:https:\/\/doi.org\/10.1145\/277650.277732 10.1145\/277650.277732","DOI":"10.1145\/277652.277732"},{"key":"#cr-split#-e_1_2_1_61_1.2","doi-asserted-by":"crossref","unstructured":"Hongwei Xi and Frank Pfenning. 1998. Eliminating array bound checking through dependent types. In PLDI'98. 249--257. DOI:https:\/\/doi.org\/10.1145\/277650.277732","DOI":"10.1145\/277652.277732"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3409805","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3409805","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:41Z","timestamp":1750199921000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3409805"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,20]]},"references-count":79,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1,31]]}},"alternative-id":["10.1145\/3409805"],"URL":"https:\/\/doi.org\/10.1145\/3409805","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2021,1,20]]},"assertion":[{"value":"2020-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}