{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:08:40Z","timestamp":1769724520170,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T00:00:00Z","timestamp":1623974400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Czech Science Foundation","award":["GJ19-15134Y"],"award-info":[{"award-number":["GJ19-15134Y"]}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["CoG 863818 (ForM-SMArt)"],"award-info":[{"award-number":["CoG 863818 (ForM-SMArt)"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,6,19]]},"DOI":"10.1145\/3453483.3454093","type":"proceedings-article","created":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T16:58:49Z","timestamp":1624553929000},"page":"1033-1048","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Proving non-termination by program reversal"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria, Austria"}]},{"given":"Ehsan Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[{"name":"Ferdowsi University of Mashhad, Iran"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5026-4392","authenticated-orcid":false,"given":"Petr","family":"Novotn\u00fd","sequence":"additional","affiliation":[{"name":"Masaryk University, Czechia"}]},{"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}]}],"member":"320","published-online":{"date-parts":[[2021,6,18]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Amir Kafshdar Goharshady, and Mohammad Mahdavi","author":"Asadi Ali","year":"2020","unstructured":"Ali Asadi , Krishnendu Chatterjee , Hongfei Fu , Amir Kafshdar Goharshady, and Mohammad Mahdavi . 2020 . Inductive Reachability Witnesses. CoRR , abs\/2007.14259 (2020), arxiv:2007.14259. arxiv:2007.14259 Ali Asadi, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Mohammad Mahdavi. 2020. Inductive Reachability Witnesses. CoRR, abs\/2007.14259 (2020), arxiv:2007.14259. arxiv:2007.14259"},{"key":"e_1_3_2_1_2_1","volume-title":"Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Ball Thomas","year":"2002","unstructured":"Thomas Ball and Sriram K. Rajamani . 2002. The SLAM project: debugging system software via static analysis . In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages , Portland, OR, USA , January 16-18, 2002 . 1\u20133. Thomas Ball and Sriram K. Rajamani. 2002. The SLAM project: debugging system software via static analysis. In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002. 1\u20133."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_27"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_6"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155095"},{"key":"e_1_3_2_1_7_1","volume-title":"17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings. 491\u2013504","author":"Bradley Aaron R.","unstructured":"Aaron R. Bradley , Zohar Manna , and Henny B. Sipma . 2005. Linear Ranking with Reachability. In Computer Aided Verification , 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings. 491\u2013504 . Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005. Linear Ranking with Reachability. In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings. 491\u2013504."},{"key":"e_1_3_2_1_8_1","volume-title":"CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. 413\u2013429","author":"Brockschmidt Marc","year":"2013","unstructured":"Marc Brockschmidt , Byron Cook , and Carsten Fuhs . 2013 . Better Termination Proving through Cooperation. In Computer Aided Verification - 25th International Conference , CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. 413\u2013429 . Marc Brockschmidt, Byron Cook, and Carsten Fuhs. 2013. Better Termination Proving through Cooperation. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. 413\u2013429."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31762-0_9"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385969"},{"key":"e_1_3_2_1_11_1","volume-title":"Petr Novotn\u00fd, and \u0110or\u0111e \u017dikeli\u0107.","author":"Chatterjee Krishnendu","year":"2021","unstructured":"Krishnendu Chatterjee , Ehsan Kafshdar Goharshady , Petr Novotn\u00fd, and \u0110or\u0111e \u017dikeli\u0107. 2021 . Proving Non-termination by Program Reversal . arxiv:2104.01189. Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotn\u00fd, and \u0110or\u0111e \u017dikeli\u0107. 2021. Proving Non-termination by Program Reversal. arxiv:2104.01189."},{"key":"e_1_3_2_1_12_1","volume-title":"TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings. 156\u2013171","author":"Chen Hong Yi","unstructured":"Hong Yi Chen , Byron Cook , Carsten Fuhs , Kaustubh Nimkar , and Peter W . O\u2019Hearn. 2014. Proving Nontermination via Safety. In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference , TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings. 156\u2013171 . Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O\u2019Hearn. 2014. Proving Nontermination via Safety. In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings. 156\u2013171."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192405"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_15_1","volume-title":"15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 420\u2013432","author":"Col\u00f3n Michael","year":"2003","unstructured":"Michael Col\u00f3n , Sriram Sankaranarayanan , and Henny Sipma . 2003 . Linear Invariant Generation Using Non-linear Constraint Solving. In Computer Aided Verification , 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 420\u2013432 . Michael Col\u00f3n, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. 420\u2013432."},{"key":"e_1_3_2_1_16_1","volume-title":"7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings. 67\u201381","author":"Col\u00f3n Michael","year":"2001","unstructured":"Michael Col\u00f3n and Henny Sipma . 2001 . Synthesis of Linear Ranking Functions. In Tools and Algorithms for the Construction and Analysis of Systems , 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings. 67\u201381 . Michael Col\u00f3n and Henny Sipma. 2001. Synthesis of Linear Ranking Functions. In Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings. 67\u201381."},{"key":"e_1_3_2_1_17_1","volume-title":"14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings. 442\u2013454","author":"Col\u00f3n Michael","year":"2002","unstructured":"Michael Col\u00f3n and Henny Sipma . 2002 . Practical Methods for Proving Program Termination. In Computer Aided Verification , 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings. 442\u2013454 . Michael Col\u00f3n and Henny Sipma. 2002. Practical Methods for Proving Program Termination. In Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings. 442\u2013454."},{"key":"e_1_3_2_1_18_1","volume-title":"FMCAD 2014","author":"Cook Byron","year":"2014","unstructured":"Byron Cook , Carsten Fuhs , Kaustubh Nimkar , and Peter W . O\u2019Hearn. 2014. Disproving termination with overapproximation. In Formal Methods in Computer-Aided Design , FMCAD 2014 , Lausanne, Switzerland , October 21-24, 2014 . 67\u201374. Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O\u2019Hearn. 2014. Disproving termination with overapproximation. In Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21-24, 2014. 67\u201374."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_1_20_1","volume-title":"TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. 47\u201361","author":"Zuleger Florian","year":"2013","unstructured":"Byron Cook, Abigail See, and Florian Zuleger . 2013 . Ramsey vs. Lexicographic Termination Proving. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference , TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. 47\u201361 . Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. Lexicographic Termination Proving. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. 47\u201361."},{"key":"e_1_3_2_1_21_1","volume-title":"6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings. 1\u201324","author":"Cousot Patrick","year":"2005","unstructured":"Patrick Cousot . 2005 . Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. In Verification, Model Checking, and Abstract Interpretation , 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings. 1\u201324 . Patrick Cousot. 2005. Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. In Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings. 1\u201324."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_23_1","volume-title":"Conference","author":"Francez Nissim","year":"1985","unstructured":"Nissim Francez , Orna Grumberg , Shmuel Katz , and Amir Pnueli . 1985 . Proving Termination of Prolog Programs. In Logics of Programs , Conference , Brooklyn College, New York, NY, USA , June 17-19, 1985, Proceedings. 89\u2013105. Nissim Francez, Orna Grumberg, Shmuel Katz, and Amir Pnueli. 1985. Proving Termination of Prolog Programs. In Logics of Programs, Conference, Brooklyn College, New York, NY, USA, June 17-19, 1985, Proceedings. 89\u2013105."},{"key":"e_1_3_2_1_24_1","volume-title":"FMCAD 2019","author":"Frohn Florian","year":"2019","unstructured":"Florian Frohn and J\u00fcrgen Giesl . 2019 . Proving Non-Termination via Loop Acceleration. In 2019 Formal Methods in Computer Aided Design , FMCAD 2019 , San Jose, CA, USA , October 22-25, 2019. 221\u2013230. Florian Frohn and J\u00fcrgen Giesl. 2019. Proving Non-Termination via Loop Acceleration. In 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019. 221\u2013230."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006","author":"Gulavani Bhargav S.","year":"2006","unstructured":"Bhargav S. Gulavani , Thomas A. Henzinger , Yamini Kannan , Aditya V. Nori , and Sriram K. Rajamani . 2006. SYNERGY: a new algorithm for property checking . In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006 , Portland, Oregon, USA , November 5-11, 2006 . 117\u2013127. Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, and Sriram K. Rajamani. 2006. SYNERGY: a new algorithm for property checking. In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, Portland, Oregon, USA, November 5-11, 2006. 117\u2013127."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328459"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_19"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_53"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209142"},{"key":"e_1_3_2_1_35_1","volume-title":"Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017","author":"Kincaid Zachary","year":"2017","unstructured":"Zachary Kincaid , Jason Breck , Ashkan Forouhi Boroujeni , and Thomas W. Reps . 2017. Compositional recurrence analysis revisited . In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017 , Barcelona, Spain , June 18-23, 2017 . 248\u2013262. Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, and Thomas W. Reps. 2017. Compositional recurrence analysis revisited. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017. 248\u2013262."},{"key":"e_1_3_2_1_36_1","volume-title":"Reps","author":"Kincaid Zachary","year":"2018","unstructured":"Zachary Kincaid , John Cyphert , Jason Breck , and Thomas W . Reps . 2018 . Non-linear reasoning for invariant synthesis. PACMPL, 2, POPL ( 2018), 54:1\u201354:33. Zachary Kincaid, John Cyphert, Jason Breck, and Thomas W. Reps. 2018. Non-linear reasoning for invariant synthesis. PACMPL, 2, POPL (2018), 54:1\u201354:33."},{"key":"e_1_3_2_1_37_1","volume-title":"CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. 779\u2013796","author":"Larraz Daniel","year":"2014","unstructured":"Daniel Larraz , Kaustubh Nimkar , Albert Oliveras , Enric Rodr\u00edguez-Carbonell , and Albert Rubio . 2014 . Proving Non-termination Using Max-SMT. In Computer Aided Verification - 26th International Conference , CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. 779\u2013796 . Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodr\u00edguez-Carbonell, and Albert Rubio. 2014. Proving Non-termination Using Max-SMT. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. 779\u2013796."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737993"},{"key":"e_1_3_2_1_39_1","volume-title":"TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. 266\u2013283","author":"Leike Jan","year":"2018","unstructured":"Jan Leike and Matthias Heizmann . 2018 . Geometric Nontermination Arguments. In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference , TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. 266\u2013283 . Jan Leike and Matthias Heizmann. 2018. Geometric Nontermination Arguments. In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. 266\u2013283."},{"key":"e_1_3_2_1_40_1","volume-title":"5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings. 239\u2013251","author":"Podelski Andreas","year":"2004","unstructured":"Andreas Podelski and Andrey Rybalchenko . 2004 . A Complete Method for the Synthesis of Linear Ranking Functions. In Verification, Model Checking, and Abstract Interpretation , 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings. 239\u2013251 . Andreas Podelski and Andrey Rybalchenko. 2004. A Complete Method for the Synthesis of Linear Ranking Functions. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings. 239\u2013251."},{"key":"e_1_3_2_1_41_1","volume-title":"Transition Invariants. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings. 32\u201341","author":"Podelski Andreas","year":"2004","unstructured":"Andreas Podelski and Andrey Rybalchenko . 2004 . Transition Invariants. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings. 32\u201341 . Andreas Podelski and Andrey Rybalchenko. 2004. Transition Invariants. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings. 32\u201341."},{"key":"e_1_3_2_1_42_1","volume-title":"International Symposium ISSAC 2004, Santander, Spain, July 4-7, 2004, Proceedings. 266\u2013273","author":"Rodr\u00edguez-Carbonell Enric","year":"2004","unstructured":"Enric Rodr\u00edguez-Carbonell and Deepak Kapur . 2004 . Automatic generation of polynomial loop. In Symbolic and Algebraic Computation , International Symposium ISSAC 2004, Santander, Spain, July 4-7, 2004, Proceedings. 266\u2013273 . Enric Rodr\u00edguez-Carbonell and Deepak Kapur. 2004. Automatic generation of polynomial loop. In Symbolic and Algebraic Computation, International Symposium ISSAC 2004, Santander, Spain, July 4-7, 2004, Proceedings. 266\u2013273."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_4"},{"key":"e_1_3_2_1_46_1","volume-title":"Second International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings. 154\u2013170","author":"Velroyen Helga","year":"2008","unstructured":"Helga Velroyen and Philipp R\u00fcmmer . 2008 . Non-termination Checking for Imperative Programs. In Tests and Proofs , Second International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings. 154\u2013170 . Helga Velroyen and Philipp R\u00fcmmer. 2008. Non-termination Checking for Imperative Programs. In Tests and Proofs, Second International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings. 154\u2013170."}],"event":{"name":"PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"Virtual Canada","acronym":"PLDI '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454093","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453483.3454093","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:48Z","timestamp":1750193268000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454093"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,18]]},"references-count":46,"alternative-id":["10.1145\/3453483.3454093","10.1145\/3453483"],"URL":"https:\/\/doi.org\/10.1145\/3453483.3454093","relation":{},"subject":[],"published":{"date-parts":[[2021,6,18]]},"assertion":[{"value":"2021-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}