{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:08Z","timestamp":1751660528385,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"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":["1521539"],"award-info":[{"award-number":["1521539"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2930"],"award-info":[{"award-number":["N00014-17-1-2930"]}],"id":[{"id":"10.13039\/100000006","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":[[2021,10,20]]},"abstract":"<jats:p>Verifying imperative programs is hard. A key difficulty is that the specification of what an imperative program does is often intertwined with details about pointers and imperative state. Although there are a number of powerful separation logics that allow the details of imperative state to be captured and managed, these details are complicated and reasoning about them requires significant time and expertise. In this paper, we take a different approach: a memory-safe type system that, as part of type-checking, extracts functional specifications from imperative programs. This disentangles imperative state, which is handled by the type system, from functional specifications, which can be verified without reference to pointers. A key difficulty is that sometimes memory safety depends crucially on the functional specification of a program; e.g., an array index is only memory-safe if the index is in bounds. To handle this case, our specification extraction inserts dynamic checks into the specification. Verification then requires the additional proof that none of these checks fail. However, these checks are in a purely functional language, and so this proof also requires no reasoning about pointers.<\/jats:p>","DOI":"10.1145\/3485512","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A type system for extracting functional specifications from memory-safe imperative programs"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6305-4335","authenticated-orcid":false,"given":"Paul","family":"He","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}]},{"given":"Eddy","family":"Westbrook","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"given":"Brent","family":"Carmer","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2021-1051","authenticated-orcid":false,"given":"Chris","family":"Phifer","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"given":"Valentin","family":"Robert","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"given":"Karl","family":"Smeltzer","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"given":"Andrei","family":"\u015etef\u0103nescu","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"given":"Aaron","family":"Tomb","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"given":"Adam","family":"Wick","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"given":"Matthew","family":"Yacavone","sequence":"additional","affiliation":[{"name":"Galois, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3516-1512","authenticated-orcid":false,"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"volume-title":"Program Logics for Certified Compilers","author":"Appel Andrew W.","key":"e_1_2_2_1_1","unstructured":"Andrew W. Appel , Robert Dockins , Aquinas Hobor , Lennart Beringer , Josiah Dodds , Gordon Stewart , Sandrine Blazy , and Xavier Leroy . 2014. Program Logics for Certified Compilers . Cambridge University Press . Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press."},{"volume-title":"Proceedings of the 34th Annual ACM Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA).","author":"Astrauskas Vytautas","key":"e_1_2_2_2_1","unstructured":"Vytautas Astrauskas , Peter M\u00fcller , Federico Poli , and Alexander J. Summers . 2019. Leveraging Rust Types for Modular Specification and Verification . In Proceedings of the 34th Annual ACM Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA). Vytautas Astrauskas, Peter M\u00fcller, Federico Poli, and Alexander J. Summers. 2019. Leveraging Rust Types for Modular Specification and Verification. In Proceedings of the 34th Annual ACM Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA)."},{"volume-title":"Proceedings of the 23rd International Symposium on Formal Methods (FM).","author":"Beringer Lennart","key":"e_1_2_2_3_1","unstructured":"Lennart Beringer and Andrew W. Appel . 2019. Abstraction and Subsumption in Modular Verification of C Programs . In Proceedings of the 23rd International Symposium on Formal Methods (FM). Lennart Beringer and Andrew W. Appel. 2019. Abstraction and Subsumption in Modular Verification of C Programs. In Proceedings of the 23rd International Symposium on Formal Methods (FM)."},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the 33rd Conference on the Mathematical Foundations of Programming Semantics.","author":"Bizjak Ale\u0161","year":"2017","unstructured":"Ale\u0161 Bizjak and Lars Birkedal . 2017 . On Models of Higher-Order Separation Logic . In Proceedings of the 33rd Conference on the Mathematical Foundations of Programming Semantics. Ale\u0161 Bizjak and Lars Birkedal. 2017. On Models of Higher-Order Separation Logic. In Proceedings of the 33rd Conference on the Mathematical Foundations of Programming Semantics."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/645869.668533"},{"key":"e_1_2_2_6_1","volume-title":"Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59","author":"Browne Michael C","year":"1988","unstructured":"Michael C Browne , Edmund Clarke , and Orna Grumberg . 1988. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59 ( 1988 ). Michael C Browne, Edmund Clarke, and Orna Grumberg. 1988. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59 (1988)."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_26"},{"volume-title":"Proceedings of the Workshop on Logics of Programs.","author":"Clarke Edmund M.","key":"e_1_2_2_9_1","unstructured":"Edmund M. Clarke and E. Allen Emerson . 1981. Design and synthesis of synchronization skeletons using branching time temporal logic . In Proceedings of the Workshop on Logics of Programs. Edmund M. Clarke and E. Allen Emerson. 1981. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the Workshop on Logics of Programs."},{"key":"e_1_2_2_10_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 1999 . Model Checking. MIT Press . Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1990.113739"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48869-1_5"},{"key":"e_1_2_2_14_1","volume-title":"Deny-Guarantee Reasoning. In 18th European Symposium on Programming (ESOP).","author":"Dodds Mike","year":"2009","unstructured":"Mike Dodds , Xinyu Feng , Matthew Parkinson , and Viktor Vafeiadis . 2009 . Deny-Guarantee Reasoning. In 18th European Symposium on Programming (ESOP). Mike Dodds, Xinyu Feng, Matthew Parkinson, and Viktor Vafeiadis. 2009. Deny-Guarantee Reasoning. In 18th European Symposium on Programming (ESOP)."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480922"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434323"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462160"},{"key":"e_1_2_2_18_1","volume-title":"Proceedings of AsiaBSDCon.","author":"Jeker Claudio","year":"2008","unstructured":"Claudio Jeker . 2008 . OpenBSD Network Stack Internals . In Proceedings of AsiaBSDCon. Claudio Jeker. 2008. OpenBSD Network Stack Internals. In Proceedings of AsiaBSDCon."},{"key":"e_1_2_2_19_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ale\u0161 Bizjak , Lars Birkedal , and Derek Dreyer . 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 ( 2018 ). Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 (2018)."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386029"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_24"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"volume-title":"Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI).","author":"M\u00fcller Peter","key":"e_1_2_2_29_1","unstructured":"Peter M\u00fcller , Malte Schwerhoff , and Alexander J. Summers . 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning . In Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)."},{"volume-title":"Proceedings of the 20th European Symposium on Programming (ESOP).","author":"Matthew","key":"e_1_2_2_30_1","unstructured":"Matthew J. Parkinson and Alexander J. Summers. 2011. The Relationship between Separation Logic and Implicit Dynamic Frames . In Proceedings of the 20th European Symposium on Programming (ESOP). Matthew J. Parkinson and Alexander J. Summers. 2011. The Relationship between Separation Logic and Implicit Dynamic Frames. In Proceedings of the 20th European Symposium on Programming (ESOP)."},{"key":"e_1_2_2_31_1","volume-title":"The Redox Operating System. https:\/\/doc.redox-os.org\/book\/ Accessed","author":"Developers Redox","year":"2020","unstructured":"Redox Developers . [n.d.]. The Redox Operating System. https:\/\/doc.redox-os.org\/book\/ Accessed : Nov 13, 2020 . Redox Developers. [n.d.]. The Redox Operating System. https:\/\/doc.redox-os.org\/book\/ Accessed: Nov 13, 2020."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_33_1","volume-title":"Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees. In 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).","author":"Silver Lucas","year":"2021","unstructured":"Lucas Silver and Steve Zdancewic . 2021 . Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees. In 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). Lucas Silver and Steve Zdancewic. 2021. Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees. In 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428220"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"volume-title":"Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis","author":"Ullrich Sebastian","key":"e_1_2_2_37_1","unstructured":"Sebastian Ullrich . 2016. Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis . Karlsruhe Institute of Technology . Sebastian Ullrich. 2016. Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis. Karlsruhe Institute of Technology."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"e_1_2_2_39_1","volume-title":"Interaction Trees. In Proceedings of the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).","author":"Zakowski Yannick","year":"2020","unstructured":"Li-yao Xia, Yannick Zakowski , Paul He , Chung-Kil Hur , Gregory Malecha , Benjamin C. Pierce , and Steve Zdancewic . 2020 . Interaction Trees. In Proceedings of the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction Trees. In Proceedings of the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485512","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485512","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485512","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485512"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":39,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485512"],"URL":"https:\/\/doi.org\/10.1145\/3485512","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}