{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:59Z","timestamp":1750221299128,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,9,5]],"date-time":"2018-09-05T00:00:00Z","timestamp":1536105600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,9,5]]},"DOI":"10.1145\/3310232.3310240","type":"proceedings-article","created":{"date-parts":[[2019,4,4]],"date-time":"2019-04-04T18:38:43Z","timestamp":1554403123000},"page":"59-70","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["ESVERIFY"],"prefix":"10.1145","author":[{"given":"Christopher","family":"Schuster","sequence":"first","affiliation":[{"name":"University of California, Santa Cruz"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sohum","family":"Banerjea","sequence":"additional","affiliation":[{"name":"University of California, Santa Cruz"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cormac","family":"Flanagan","sequence":"additional","affiliation":[{"name":"University of California, Santa Cruz"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,9,5]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Blame for All. In POPL '11","author":"Ahmed Amal","year":"2011","unstructured":"Amal Ahmed , Robert Bruce Findler , Jeremy G. Siek , and Philip Wadler . 2011 . Blame for All. In POPL '11 . Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for All. In POPL '11."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660214"},{"key":"e_1_3_2_1_3_1","volume-title":"CVC Lite: A New Implementation of the Cooperating Validity Checker. In CAV'04","author":"Barrett Clark","year":"2004","unstructured":"Clark Barrett and Sergey Berezin . 2004 . CVC Lite: A New Implementation of the Cooperating Validity Checker. In CAV'04 . Clark Barrett and Sergey Berezin. 2004. CVC Lite: A New Implementation of the Cooperating Validity Checker. In CAV'04."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384659"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9352-2"},{"key":"e_1_3_2_1_9_1","unstructured":"ECMA-262. 2017. ECMAScript 2017 Language Specification (6 \/ 2017 ed.).  ECMA-262. 2017. ECMAScript 2017 Language Specification (6 \/ 2017 ed.)."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158138"},{"key":"e_1_3_2_1_14_1","unstructured":"Carlo Alberto Furia and Bertrand Meyer. 2010. Inferring Loop Invariants Using Post-conditions. In Fields of Logic and Computation.  Carlo Alberto Furia and Bertrand Meyer. 2010. Inferring Loop Invariants Using Post-conditions. In Fields of Logic and Computation."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_3_2_1_16_1","series-title":"Lecture Notes in Computer Science","volume-title":"ECOOP 2003 Object-Oriented Programming, Luca Cardelli (Ed.)","author":"Henkel Johannes","unstructured":"Johannes Henkel and Amer Diwan . 2003. Discovering Algebraic Specifications from Java Classes . In ECOOP 2003 Object-Oriented Programming, Luca Cardelli (Ed.) . Lecture Notes in Computer Science , Vol. 2743 . Springer Berlin Heidelberg , 431--456. Johannes Henkel and Amer Diwan. 2003. Discovering Algebraic Specifications from Java Classes. In ECOOP 2003 Object-Oriented Programming, Luca Cardelli (Ed.). Lecture Notes in Computer Science, Vol. 2743. Springer Berlin Heidelberg, 431--456."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_3_2_1_18_1","unstructured":"K. Rustan M. Leino. 2001. Extended Static Checking: A Ten-Year Perspective. In Informatics - 10 Years Back. 10 Years Ahead.   K. Rustan M. Leino. 2001. Extended Static Checking: A Ten-Year Perspective. In Informatics - 10 Years Back. 10 Years Ahead."},{"key":"e_1_3_2_1_19_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10).","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino . 2010 . Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10). K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'10)."},{"key":"e_1_3_2_1_20_1","volume-title":"Developing Verified Programs with Dafny. In International Conference on Software Engineering, (ICSE'13)","author":"Leino K. Rustan M.","year":"2013","unstructured":"K. Rustan M. Leino . 2013 . Developing Verified Programs with Dafny. In International Conference on Software Engineering, (ICSE'13) . K. Rustan M. Leino. 2013. Developing Verified Programs with Dafny. In International Conference on Software Engineering, (ICSE'13)."},{"key":"e_1_3_2_1_21_1","volume-title":"Accessible Software Verification with Dafny","author":"Leino K. Rustan M.","year":"2017","unstructured":"K. Rustan M. Leino . 2017. Accessible Software Verification with Dafny . IEEE Software ( 2017 ). K. Rustan M. Leino. 2017. Accessible Software Verification with Dafny. IEEE Software (2017)."},{"volume-title":"CAV'16","author":"K. Rustan","key":"e_1_3_2_1_22_1","unstructured":"K. Rustan M. Leino and Cl\u00e9ment Pit-Claudel. 2016. Trigger selection strategies to stabilize program verifiers . In CAV'16 . K. Rustan M. Leino and Cl\u00e9ment Pit-Claudel. 2016. Trigger selection strategies to stabilize program verifiers. In CAV'16."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54016"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_1_25_1","volume-title":"ECOOP'15","author":"Park Changhee","year":"2015","unstructured":"Changhee Park and Sukyoung Ryu . 2015 . Scalable and Precise Static Analysis of JavaScript Applications via Loop-Sensitivity . In ECOOP'15 . Changhee Park and Sukyoung Ryu. 2015. Scalable and Precise Static Analysis of JavaScript Applications via Loop-Sensitivity. In ECOOP'15."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_26"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_19"},{"volume-title":"Gradual Typing for Functional Languages. In Workshop on Scheme and Functional Programming.","author":"Jeremy","key":"e_1_3_2_1_28_1","unstructured":"Jeremy G. Siek and Walid Taha. 2006 . Gradual Typing for Functional Languages. In Workshop on Scheme and Functional Programming. Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Workshop on Scheme and Functional Programming."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792786.1792798"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122963"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"}],"event":{"name":"IFL 2018: 30th Symposium on Implementation and Application of Functional Languages","acronym":"IFL 2018","location":"Lowell MA USA"},"container-title":["Proceedings of the 30th Symposium on Implementation and Application of Functional Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310232.3310240","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3310232.3310240","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:16Z","timestamp":1750212796000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3310232.3310240"}},"subtitle":["Verifying Dynamically-Typed Higher-Order Functional Programs by SMT Solving"],"short-title":[],"issued":{"date-parts":[[2018,9,5]]},"references-count":33,"alternative-id":["10.1145\/3310232.3310240","10.1145\/3310232"],"URL":"https:\/\/doi.org\/10.1145\/3310232.3310240","relation":{},"subject":[],"published":{"date-parts":[[2018,9,5]]},"assertion":[{"value":"2018-09-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}