{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:48Z","timestamp":1784837808540,"version":"3.55.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-SHF 2321680"],"award-info":[{"award-number":["CCF-SHF 2321680"]}],"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":[[2024,6,20]]},"abstract":"<jats:p>Functional programs typically interact with stateful libraries that hide state behind typed abstractions. One particularly important class of applications are data structure implementations that rely on such libraries to provide a level of efficiency and scalability that may be otherwise difficult to achieve. However, because the specifications of the methods provided by these libraries are necessarily general and rarely specialized to the needs of any specific client, any required application-level invariants must often be expressed in terms of additional constraints on the (often) opaque state maintained by the library.<\/jats:p>\n          <jats:p>\n            In this paper, we consider the specification and verification of such\n            <jats:italic toggle=\"yes\">representation invariants<\/jats:italic>\n            using\n            <jats:italic toggle=\"yes\">symbolic finite automata<\/jats:italic>\n            (SFA). We show that SFAs can be used to succinctly and precisely capture fine-grained temporal and data-dependent histories of interactions between functional clients and stateful libraries. To facilitate modular and compositional reasoning, we integrate SFAs into a refinement type system to qualify stateful computations resulting from such interactions. The particular instantiation we consider,\n            <jats:italic toggle=\"yes\">Hoare Automata Types<\/jats:italic>\n            (HATs), allows us to both specify and automatically type-check the representation invariants of a datatype, even when its implementation depends on stateful library methods that operate over hidden state.\n          <\/jats:p>\n          <jats:p>We also develop a new bidirectional type checking algorithm that implements an efficient subtyping inclusion check over HATs, enabling their translation into a form amenable for SMT-based automated verification. We present extensive experimental results on an implementation of this algorithm that demonstrates the feasibility of type-checking complex and sophisticated HAT-specified OCaml data structure implementations layered on top of stateful library APIs.<\/jats:p>","DOI":"10.1145\/3656433","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1387-1411","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3900-7501","authenticated-orcid":false,"given":"Zhe","family":"Zhou","sequence":"first","affiliation":[{"name":"Purdue University, WEST LAFAYETTE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5977-5236","authenticated-orcid":false,"given":"Qianchuan","family":"Ye","sequence":"additional","affiliation":[{"name":"Purdue University, WEST LAFAYETTE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1016-6261","authenticated-orcid":false,"given":"Benjamin","family":"Delaware","sequence":"additional","affiliation":[{"name":"Purdue University, WEST LAFAYETTE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6871-2424","authenticated-orcid":false,"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, WEST LAFAYETTE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1889999"},{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40206-7_1"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0183-5"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571254"},{"key":"e_1_3_1_6_1","article-title":"VOCAL \u2013 A Verified OCaml Library","author":"Chargu\u00e9raud Arthur","year":"2017","unstructured":"Arthur Chargu\u00e9raud, Jean-Christophe Filli\u00e2tre, M\u00e1rio Pereira, and Fran\u00e7ois Pottier. 2017. VOCAL \u2013 A Verified OCaml Library. ML Family Workshop. https:\/\/hal.inria.fr\/hal-01561094","journal-title":"ML Family Workshop."},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_14"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535849"},{"key":"e_1_3_1_9_1","first-page":"854","volume-title":"Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (Beijing, China) (I7CAI \u201813)","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 Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (Beijing, China) (I7CAI \u201813). AAAI Press, 854\u2013860. https:\/\/doi.org\/10.5555\/2540128.2540252"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24851-4_21"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing. ACM Comput. Surv. 54 5 Article 98 (may 2021) 38 pages. https:\/\/doi.org\/10.1145\/3450952 10.1145\/3450952","DOI":"10.1145\/3450952"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Loris D\u2019 Antoni and Margus Veanes. 2017. The Power of Symbolic Automata and Transducers. In Computer Aided Verification: 29th International Conference CAV 2017 Heidelberg Germany July 24-28 2017 Proceedings Part I 30. Springer 47\u201367. https:\/\/doi.org\/10.1007\/978-3-319-63387-9_3 10.1007\/978-3-319-63387-9_3","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473590"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319848"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178053"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Hossein Hojjat and Philipp R\u00fcmmer. 2018. The ELDARICA Horn Solver. In 2018 Formal Methods in Computer Aided Design FMCAD 2018 Austin TX USA October 30 - November 2 2018 Nikolaj S. Bj\u00f8rner and Arie Gurfinkel (Eds.). IEEE 1\u20137. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013 10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_3_1_22_1","unstructured":"Java 2013. Java Platform Standard Edition 7 Documentation. https:\/\/docs.oracle.com\/javase\/7\/docs\/"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603138"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547632"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_5"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Anders Miltner Saswat Padhi Todd D. Millstein and David Walker. 2020. Data-driven Inference of Representation Invariants. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation PLDI 2020 London UK June 15-20 2020 Alastair F. Donaldson and Emina Torlak (Eds.). ACM 1\u201315. https:\/\/doi.org\/10.1145\/3385412.3385967 10.1145\/3385412.3385967","DOI":"10.1145\/3385412.3385967"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27810-0_1"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Aleksandar Nanevski Greg Morrisett Avraham Shinnar Paul Govereau and Lars Birkedal. 2008b. Ynot: Dependent Types for Imperative Programs. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP \u201808). Association for Computing Machinery New York NY USA 229\u2013240. https:\/\/doi.org\/10.1145\/1411204.1411237 10.1145\/1411204.1411237","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/580840"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4842-8_1"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076021.2048122"},{"key":"e_1_3_1_39_1","unstructured":"Nikhil Swamy Guido Martinez and Aseem Rastogi. 2023. Proof-Oriented Programming in F\u2217. https:\/\/fstar-lang.org\/tutorial\/ proof-oriented-programming-in-fstar.pdf"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Nikhil Swamy Joel Weinberger Cole Schlesinger Juan Chen and Benjamin Livshits. 2013. Verifying Higher-Order Programs with the Dijkstra Monad. In ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI \u201813 Seattle WA USA June 16-19 2013 Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM 387\u2013398. https:\/\/doi.org\/10.1145\/2491956.2491978 10.1145\/2491956.2491978","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429074"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.18"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Vasco T. Vasconcelos. 2009. Fundamentals of Session Types. Springer Berlin Heidelberg Berlin Heidelberg 158\u2013186. https:\/\/doi.org\/10.1007\/978-3-642-01918-0_4 10.1007\/978-3-642-01918-0_4","DOI":"10.1007\/978-3-642-01918-0_4"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628161"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39274-0_3"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8_45"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122962"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.32"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485493"},{"key":"e_1_3_1_52_1","article-title":"A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata","author":"Zhou Zhe","year":"2024","unstructured":"Zhe Zhou, Qianchuan Ye, Benjamin Delaware, and Suresh Jagannathan. 2024a. A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata. arXiv:2404.01484 [cs.PL]","journal-title":"arXiv:2404.01484 [cs.PL]"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","unstructured":"Zhe Zhou Qianchuan Ye Benjamin Delaware and Suresh Jagannathan. 2024b. PLDI2024 Artifact: A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata. https:\/\/doi.org\/10.5281\/zenodo.10806686 10.5281\/zenodo.10806686","DOI":"10.5281\/zenodo.10806686"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","unstructured":"He Zhu Stephen Magill and Suresh Jagannathan. 2018. A data-driven CHC solver. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2018 Philadelphia PA USA June 18-22 2018 Jeffrey S. Foster and Dan Grossman (Eds.). ACM 707\u2013721. https:\/\/doi.org\/10.1145\/3192366.3192416 10.1145\/3192366.3192416","DOI":"10.1145\/3192366.3192416"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656433","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656433","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:39:02Z","timestamp":1751661542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656433"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":54,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656433"],"URL":"https:\/\/doi.org\/10.1145\/3656433","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}