{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T00:39:14Z","timestamp":1790987954610,"version":"4.1.0"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2315363, 2107169, 2008633, and 2304758"],"award-info":[{"award-number":["2315363, 2107169, 2008633, and 2304758"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    This paper describes a new\n                    <jats:italic toggle=\"yes\">abstract interpretation<\/jats:italic>\n                    -based approach to verify temporal safety properties of recursive, higher-order programs. While prior works have provided theoretical impact and some automation, they have had limited scalability. We begin with a new automata-based \u201cabstract effect domain\u201d for summarizing context-sensitive dependent effects, capable of abstracting relations between the program environment and the automaton control state. Our analysis includes a new transformer for abstracting event prefixes to automatically computed context-sensitive effect summaries, and is instantiated in a type-and-effect system grounded in abstract interpretation. Since the analysis is parametric on the automaton, we next instantiate it to a broader class of history\/register (or \u201caccumulator\u201d) automata, beyond finite state automata to express some context-free properties, input-dependency, event summation, resource usage, cost, equal event magnitude, etc.\n                  <\/jats:p>\n                  <jats:p>\n                    We implemented a prototype\n                    <jats:bold>ev<\/jats:bold>\n                    <jats:sc>Drift<\/jats:sc>\n                    that computes dependent effect summaries (and validates assertions) for OCaml-like recursive higher-order programs. As a basis of comparison, we describe reductions to assertion checking for higher-order but effect-free programs, and demonstrate that our approach outperforms prior tools\n                    <jats:sc>Drift<\/jats:sc>\n                    ,\n                    <jats:sc>RCaml<\/jats:sc>\n                    \/\n                    <jats:sc>Spacer<\/jats:sc>\n                    ,\n                    <jats:sc>MoCHi<\/jats:sc>\n                    , and\n                    <jats:sc>ReTHFL<\/jats:sc>\n                    . Overall, across a set of 23 benchmarks,\n                    <jats:sc>Drift<\/jats:sc>\n                    verified 12 benchmarks,\n                    <jats:sc>RCaml\/Spacer<\/jats:sc>\n                    verified 6,\n                    <jats:sc>MoCHi<\/jats:sc>\n                    verified 11,\n                    <jats:sc>ReTHFL<\/jats:sc>\n                    verified 18, and\n                    <jats:bold>ev<\/jats:bold>\n                    <jats:sc>Drift<\/jats:sc>\n                    verified 21;\n                    <jats:bold>ev<\/jats:bold>\n                    <jats:sc>Drift<\/jats:sc>\n                    also achieved a 6.3\u00d7, 5.3\u00d7, 16.8\u00d7, and 6.4\u00d7 speedup over\n                    <jats:sc>Drift<\/jats:sc>\n                    ,\n                    <jats:sc>RCami\/Spacer<\/jats:sc>\n                    ,\n                    <jats:sc>MoCHi<\/jats:sc>\n                    , and\n                    <jats:sc>ReTHFL<\/jats:sc>\n                    , respectively, on those benchmarks that both tools could solve.\n                  <\/jats:p>","DOI":"10.1145\/3763140","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"2511-2539","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Abstract Interpretation of Temporal Safety Effects of Higher Order Programs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0204-1626","authenticated-orcid":false,"given":"Mihai","family":"Nicola","sequence":"first","affiliation":[{"name":"Stevens Institute of Technology, Hoboken, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-0921-697X","authenticated-orcid":false,"given":"Chaitanya","family":"Agarwal","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7363-634X","authenticated-orcid":false,"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, Hoboken, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4051-5968","authenticated-orcid":false,"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71410-1_16"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2007.08.001"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30201-8_11"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","unstructured":"D. Beyer. 2024. State of the Art in Software Verification and Witness Validation: SV-COMP 2024. In Proc. TACAS (3) (LNCS 14572). Springer 299\u2013329. doi:10.1007\/978-3-031-57256-2_15","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"e_1_3_1_6_2","unstructured":"Bruno Blanchet Patrick Cousot Radhia Cousot J\u00e9r\u00f4me Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2007. A Static Analyzer for Large Safety-Critical Software. CoRR abs\/cs\/0701193 (2007). arXiv:cs\/0701193 http:\/\/arxiv.org\/abs\/cs\/0701193"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","unstructured":"Michael Borkowski Niki Vazou and Ranjit Jhala. 2024. Mechanizing Refinement Types. Proc. ACM Program. Lang. 8 POPL (2024) 2099\u20132128. doi:10.1145\/3632912","DOI":"10.1145\/3632912"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","unstructured":"Ugo Dal Lago and Alexis Ghyselen. 2024. On Model-Checking Higher-Order Effectful Programs. Proc. ACM Program. Lang. 8 POPL (2024) 2610\u20132638. doi:10.1145\/3632929","DOI":"10.1145\/3632929"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_1"},{"key":"e_1_3_1_11_2","volume-title":"Grid domains for analysing software","author":"Dobson Katy Louise","year":"2008","unstructured":"Katy Louise Dobson. 2008. Grid domains for analysing software. Ph. D. Dissertation. University of Leeds, UK. http:\/\/etheses.whiterose.ac.uk\/1370\/"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434298"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781169"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_1_15_2","first-page":"854","volume-title":"IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013","author":"De Giacomo Giuseppe","year":"2013","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, Francesca Rossi (Ed.). IJCAI\/AAAI, 854\u2013860. http:\/\/www.aaai.org\/ocs\/index.php\/IJCAI\/IJCAI13\/paper\/view\/6997"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2017.13"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_16"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603127"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1057387.1057390"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"e_1_3_1_25_2","unstructured":"Ranjit Jhala. 2025. LiquidHaskell. https:\/\/ucsd-progsys.github.io\/liquidhaskell\/"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64437-6_5"},{"key":"e_1_3_1_29_2","unstructured":"Hiroyuki Katsura Naoki Iwayama Naoki Kobayashi and Takeshi Tsukada. 2025. ReTHFL. https:\/\/github.com\/hopv\/rethfl"},{"key":"e_1_3_1_30_2","unstructured":"Hiroyuki Katsura Naoki Iwayama Naoki Kobayashi and Takeshi Tsukada. 2025. Web interface for ReTHFL. https:\/\/www-kb.is.s.u-tokyo.ac.jp\/~koba\/nuhfl\/"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3633280"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1481848.1481853"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571199"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_25"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603138"},{"key":"e_1_3_1_38_2","doi-asserted-by":"crossref","unstructured":"Satoshi Kura and Hiroshi Unno. 2024. Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System. arXiv:2407.02975 [cs.LO] https:\/\/arxiv.org\/abs\/2407.02975","DOI":"10.1145\/3674662"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_21"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632929"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"e_1_3_1_43_2","article-title":"The Octagon Abstract Domain","author":"Min\u00e9 Antoine","year":"2007","unstructured":"Antoine Min\u00e9. 2007. The Octagon Abstract Domain. CoRR abs\/cs\/0703084 (2007). arXiv:cs\/0703084 http:\/\/arxiv.org\/abs\/cs\/0703084","journal-title":"CoRR abs\/cs\/0703084"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837667"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158139"},{"key":"e_1_3_1_47_2","doi-asserted-by":"crossref","unstructured":"Mihai Nicola Chaitanya Agarwal Eric Koskinen and Thomas Wies. 2025. Abstract Interpretation of Temporal Safety Effects of Higher Order Programs [Extended Version]. (2025). arXiv:2408.02791 [cs.PL]","DOI":"10.1145\/3763140"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","unstructured":"Mihai Nicola Chaitanya Agarwal Eric Koskinen and Thomas Wies. 2025. The evDrift Verifier. Zenodo. doi:10.5281\/zenodo.16602546","DOI":"10.5281\/zenodo.16602546"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80969-1"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434300"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_1_54_2","unstructured":"Ryosuke Sato. 2025. MoCHi. https:\/\/github.com\/hopv\/mochi"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009885"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006466"},{"key":"e_1_3_1_59_2","unstructured":"sosy lab. 2025. benchexec. https:\/\/github.com\/sosy-lab\/benchexec"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00085"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_1_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429074"},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706315"},{"key":"e_1_3_1_64_2","unstructured":"Hiroshi Unno. 2025. CoAR. https:\/\/github.com\/hiroshi-unno\/coar\/"},{"key":"e_1_3_1_65_2","first-page":"167","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS \u201987), Ithaca, New York, USA, June 22-25, 1987","author":"Vardi Moshe Y.","year":"1987","unstructured":"Moshe Y. Vardi. 1987. Verification of Concurrent Programs: The Automata-Theoretic Framework. In Proceedings of the Symposium on Logic in Computer Science (LICS \u201987), Ithaca, New York, USA, June 22-25, 1987. IEEE Computer Society, 167\u2013176."},{"key":"e_1_3_1_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-91121-7_16"},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656433"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763140","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763140","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:15:10Z","timestamp":1784196910000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763140"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":68,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763140"],"URL":"https:\/\/doi.org\/10.1145\/3763140","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}