{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:22:18Z","timestamp":1770290538199,"version":"3.49.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1618756"],"award-info":[{"award-number":["1618756"]}],"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":[[2018,1]]},"abstract":"<jats:p>Software contracts allow programmers to state rich program properties using the full expressive power of an object language. However, since they are enforced at runtime, monitoring contracts imposes significant overhead and delays error discovery. So contract veri cation aims to guarantee all or most of these properties ahead of time, enabling valuable optimizations and yielding a more general assurance of correctness. Existing methods for static contract verification satisfy the needs of more restricted target languages, but fail to address the challenges unique to those conjoining untyped, dynamic programming, higher-order functions, modularity, and statefulness. Our approach tackles all these features at once, in the context of the full Racket system\u2014a mature environment for stateful, higher-order, multi-paradigm programming with or with- out types. Evaluating our method using a set of both pure and stateful benchmarks, we are able to verify 99.94% of checks statically (all but 28 of 49, 861).<\/jats:p>\n          <jats:p>Stateful, higher-order functions pose significant challenges for static contract verification in particular. In the presence of these features, a modular analysis must permit code from the current module to escape permanently to an opaque context (unspecified code from outside the current module) that may be stateful and therefore store a reference to the escaped closure. Also, contracts themselves, being predicates wri en in unrestricted Racket, may exhibit stateful behavior; a sound approach must be robust to contracts which are arbitrarily expressive and interwoven with the code they monitor. In this paper, we present and evaluate our solution based on higher-order symbolic execution, explain the techniques we used to address such thorny issues, formalize a notion of behavioral approximation, and use it to provide a mechanized proof of soundness.<\/jats:p>","DOI":"10.1145\/3158139","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Soft contract verification for higher-order stateful programs"],"prefix":"10.1145","volume":"2","author":[{"given":"Ph\u00fac C.","family":"Nguy\u1ec5n","sequence":"first","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Thomas","family":"Gilray","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Sam","family":"Tobin-Hochstadt","sequence":"additional","affiliation":[{"name":"Indiana University, USA"}]},{"given":"David","family":"Van Horn","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048136"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_15"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_2_2_4_1","volume-title":"Computer Aided Verification","author":"Barrett Clark","unstructured":"Clark Barrett , Christopher L Conway , Morgan Deters , Liana Hadarean , Dejan Jovanovi\u0107 , Tim King , Andrew Reynolds , and Cesare Tinelli . 2011. CVC4 . In Computer Aided Verification . Springer , 171\u2013177. Clark Barrett, ChristopherL Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\u0107, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification. Springer, 171\u2013177."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_29"},{"key":"e_1_2_2_6_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. USENIX Association, 209\u2013224","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs . In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. USENIX Association, 209\u2013224 . Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. USENIX Association, 209\u2013224."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384659"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103686"},{"key":"e_1_2_2_10_1","volume-title":"Static Determination of Dynamic Properties of Programs. In 2nd International Symposium on Programming. 106\u2013130","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot . 1976 . Static Determination of Dynamic Properties of Programs. In 2nd International Symposium on Programming. 106\u2013130 . P. Cousot and R. Cousot. 1976. Static Determination of Dynamic Properties of Programs. In 2nd International Symposium on Programming. 106\u2013130."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926410"},{"key":"e_1_2_2_13_1","volume-title":"contracts.coffee. (July","author":"Disney Tim","year":"2013","unstructured":"Tim Disney . 2013. contracts.coffee. (July 2013 ). http:\/\/disnetdev.com\/contracts.coffee\/ Tim Disney. 2013. contracts.coffee. (July 2013). http:\/\/disnetdev.com\/contracts.coffee\/"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18070-5_2"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_2_2_16_1","volume-title":"Reference: Racket. Technical Report PLT-TR-2010-1","author":"Flatt Matthew","year":"2010","unstructured":"Matthew Flatt and PLT. 2010 . Reference: Racket. Technical Report PLT-TR-2010-1 . PLT Inc . Matthew Flatt and PLT. 2010. Reference: Racket. Technical Report PLT-TR-2010-1. PLT Inc."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951936"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837631"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706341"},{"key":"e_1_2_2_21_1","unstructured":"Jessica Gronski and Cormac Flanagan. 2007. Unifying Hybrid Types and Contracts.. In Trends in Functional Programming. Citeseer 54\u201370.  Jessica Gronski and Cormac Flanagan. 2007. Unifying Hybrid Types and Contracts.. In Trends in Functional Programming. Citeseer 54\u201370."},{"key":"e_1_2_2_22_1","volume-title":"core.contracts. (July","author":"Hickey Rich","year":"2013","unstructured":"Rich Hickey , Michael Fogus , and contributors. 2013. core.contracts. (July 2013 ). https:\/\/github.com\/clojure\/core.contracts Rich Hickey, Michael Fogus, and contributors. 2013. core.contracts. (July 2013). https:\/\/github.com\/clojure\/core.contracts"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599415"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480933"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_24"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706355"},{"key":"e_1_2_2_31_1","volume-title":"A fully abstract trace semantics for general references. Automata, Languages and Programming","author":"Laird James","year":"2007","unstructured":"James Laird . 2007. A fully abstract trace semantics for general references. Automata, Languages and Programming ( 2007 ), 667\u2013679. James Laird. 2007. A fully abstract trace semantics for general references. Automata, Languages and Programming (2007), 667\u2013679."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.41"},{"key":"e_1_2_2_33_1","volume-title":"The Language","author":"Meyer Bertrand","unstructured":"Bertrand Meyer . 1991. Eiffel : The Language . Prentice Hall . Bertrand Meyer. 1991. Eiffel : The Language. Prentice Hall."},{"key":"e_1_2_2_34_1","volume-title":"International Symposium on Static Analysis (SAS). Springer, 407\u2013421","author":"Might Matthew","year":"2011","unstructured":"Matthew Might . 2011 . Abstract interpreters for free . In International Symposium on Static Analysis (SAS). Springer, 407\u2013421 . Matthew Might. 2011. Abstract interpreters for free. In International Symposium on Static Analysis (SAS). Springer, 407\u2013421."},{"key":"e_1_2_2_35_1","volume-title":"Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 260\u2013274","author":"Might Matthew","year":"2009","unstructured":"Matthew Might and Panagiotis Manolios . 2009 . A Posteriori Soundness for Non-deterministic Abstract Interpretations . In Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 260\u2013274 . Matthew Might and Panagiotis Manolios. 2009. A Posteriori Soundness for Non-deterministic Abstract Interpretations. In Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 260\u2013274."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111049"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_8"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364578"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737971"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_43_1","volume-title":"Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE, 81\u201390","author":"Luke Ong C. H.","year":"2006","unstructured":"C. H. Luke Ong . 2006 . On Model-Checking Trees Generated by Higher-Order Recursion Schemes . In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE, 81\u201390 . C. H. Luke Ong. 2006. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE, 81\u201390."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926453"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.1997.640178"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009875"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676996"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321746"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384685"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863561"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384655"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_24"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863553"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/239912.239917"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103767"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480889"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158139","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158139","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158139","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158139"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":61,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158139"],"URL":"https:\/\/doi.org\/10.1145\/3158139","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}