{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:05Z","timestamp":1772164085407,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":84,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009874","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"330-343","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Contract-based resource verification for higher-order functions with memoization"],"prefix":"10.1145","author":[{"given":"Ravichandhran","family":"Madhavan","sequence":"first","affiliation":[{"name":"EPFL, Switzerland"}]},{"given":"Sumith","family":"Kulal","sequence":"additional","affiliation":[{"name":"IIT Bombay, India"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882102"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_27"},{"key":"e_1_3_2_1_4_1","volume-title":"Quicksort and k-th smallest elements","author":"Apfelmus H.","year":"2009","unstructured":"H. Apfelmus . Quicksort and k-th smallest elements . 2009 . H. Apfelmus. Quicksort and k-th smallest elements. 2009."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/226060.226069"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69562"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"e_1_3_2_1_8_1","first-page":"177","volume-title":"CAV","author":"Barrett C.","year":"2011","unstructured":"C. Barrett , C. L. Conway , M. Deters , L. Hadarean , D. Jovanovi\u00b4c , T. King , A. Reynolds , and C. Tinelli . CVC4. In Computer Aided Verification , CAV , pages 171\u2013 177 , 2011 . C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi\u00b4c, T. King, A. Reynolds, and C. Tinelli. CVC4. In Computer Aided Verification, CAV, pages 171\u2013177, 2011."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.022"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_1_11_1","volume-title":"CAV","author":"Beyene T. A.","year":"2013","unstructured":"T. A. Beyene , C. Popeea , and A. Rybalchenko . Solving existentially quantified horn clauses. In Computer Aided Verification , CAV , 2013 . T. A. Beyene, C. Popeea, and A. Rybalchenko. Solving existentially quantified horn clauses. In Computer Aided Verification, CAV, 2013."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/113903"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2489837.2489838"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784732"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_15"},{"key":"e_1_3_2_1_16_1","first-page":"225","volume-title":"CAV","author":"Bogudlov I.","year":"2007","unstructured":"I. Bogudlov , T. Lev-Ami , T. W. Reps , and M. Sagiv . Revamping TVLA: making parametric shape analysis competitive. In Computer Aided Verification , CAV , pages 221\u2013 225 , 2007 . I. Bogudlov, T. Lev-Ami, T. W. Reps, and M. Sagiv. Revamping TVLA: making parametric shape analysis competitive. In Computer Aided Verification, CAV, pages 221\u2013225, 2007."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2866575"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594301"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_1_20_1","volume-title":"CAV","author":"Col\u00b4on M.","year":"2003","unstructured":"M. Col\u00b4on , S. Sankaranarayanan , and H. Sipma . Linear invariant generation using non-linear constraint solving. In Computer Aided Verification , CAV , 2003 . M. Col\u00b4on, S. Sankaranarayanan, and H. Sipma. Linear invariant generation using non-linear constraint solving. In Computer Aided Verification, CAV, 2003."},{"key":"e_1_3_2_1_21_1","volume-title":"Introduction to Algorithms","author":"Cormen T. H.","year":"2001","unstructured":"T. H. Cormen , C. E. Leiserson , R. L. Rivest , and C. Stein . Introduction to Algorithms ( Second Edition). MIT Press and McGraw-Hill , 2001 . T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms (Second Edition). MIT Press and McGraw-Hill, 2001."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2428116.2428123"},{"key":"e_1_3_2_1_24_1","volume-title":"Algorithms","author":"Dasgupta S.","year":"2008","unstructured":"S. Dasgupta , C. H. Papadimitriou , and U. V. Vazirani . Algorithms . McGraw-Hill , 2008 . S. Dasgupta, C. H. Papadimitriou, and U. V. Vazirani. Algorithms. McGraw-Hill, 2008."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_3_2_1_27_1","first-page":"58","volume-title":"International Workshop on Aliasing, Confinement and Ownership in Object-oriented Programming, IWACO","author":"F\u00e4hndrich M.","year":"2003","unstructured":"M. F\u00e4hndrich and K. R. M. Leino . Heap monotonic typestates . In International Workshop on Aliasing, Confinement and Ownership in Object-oriented Programming, IWACO , page 58 , 2003 . M. F\u00e4hndrich and K. R. M. Leino. Heap monotonic typestates. In International Workshop on Aliasing, Confinement and Ownership in Object-oriented Programming, IWACO, page 58, 2003."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_3_2_1_29_1","first-page":"295","volume-title":"APLAS","author":"Flores-Montoya A.","year":"2014","unstructured":"A. Flores-Montoya and R. H\u00e4hnle . Resource analysis of complex programs with cost equations. In Programming Languages and Systems - 12th Asian Symposium , APLAS , pages 275\u2013 295 , 2014 . A. Flores-Montoya and R. H\u00e4hnle. Resource analysis of complex programs with cost equations. In Programming Languages and Systems - 12th Asian Symposium, APLAS, pages 275\u2013295, 2014."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581483"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890030"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_3_2_1_33_1","volume-title":"CAV","author":"Gurfinkel A.","year":"2015","unstructured":"A. Gurfinkel , T. Kahsai , A. Komuravelli , and J. A. Navas . The SeaHorn verification framework. In Compuer Aided Verification , CAV , 2015 . A. Gurfinkel, T. Kahsai, A. Komuravelli, and J. A. Navas. The SeaHorn verification framework. In Compuer Aided Verification, CAV, 2015."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1540610"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986314"},{"key":"e_1_3_2_1_37_1","first-page":"23","volume-title":"RTA","author":"Jones N. D.","year":"2004","unstructured":"N. D. Jones and N. Bohr . Termination analysis of the untyped lambacalculus. In Rewriting Techniques and Applications , RTA , pages 1\u2013 23 , 2004 . N. D. Jones and N. Bohr. Termination analysis of the untyped lambacalculus. In Rewriting Techniques and Applications, RTA, pages 1\u201323, 2004."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181789"},{"key":"e_1_3_2_1_40_1","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann M.","year":"2000","unstructured":"M. Kaufmann , J. S. Moore , and P. Manolios . Computer-Aided Reasoning: An Approach . Kluwer Academic Publishers , Norwell, MA, USA , 2000 . M. Kaufmann, J. S. Moore, and P. Manolios. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell, MA, USA, 2000."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596566"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667051"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42347"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_27"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_50_1","volume-title":"EPFL-REPORT- 215783. Technical report","author":"Madhavan R.","year":"2016","unstructured":"R. Madhavan , S. Kulal , and V. Kuncak . Verifying resource bounds of programs with lazy evaluation and memoization , EPFL-REPORT- 215783. Technical report , EPFL , 2016 . R. Madhavan, S. Kulal, and V. Kuncak. Verifying resource bounds of programs with lazy evaluation and memoization, EPFL-REPORT- 215783. Technical report, EPFL, 2016."},{"key":"e_1_3_2_1_51_1","volume-title":"EPFL-REPORT-190578. Technical report","author":"Madhavan R.","year":"2014","unstructured":"R. Madhavan and V. Kuncak . Symbolic resource bound inference , EPFL-REPORT-190578. Technical report , EPFL , 2014 . R. Madhavan and V. Kuncak. Symbolic resource bound inference, EPFL-REPORT-190578. Technical report, EPFL, 2014."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_51"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1778180.1778211"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737971"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.5555\/1791547"},{"key":"e_1_3_2_1_57_1","volume-title":"Programming in Scala: a comprehensive step-by-step guide","author":"Odersky M.","year":"2008","unstructured":"M. Odersky , L. Spoon , and B. Venners . Programming in Scala: a comprehensive step-by-step guide . Artima Press , 2008 . M. Odersky, L. Spoon, and B. Venners. Programming in Scala: a comprehensive step-by-step guide. Artima Press, 2008."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001489"},{"key":"e_1_3_2_1_59_1","volume-title":"Cambridge University Press","author":"Okasaki C.","year":"1998","unstructured":"C. Okasaki . Purely Functional Data Structures . Cambridge University Press , 1998 . C. Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998."},{"key":"e_1_3_2_1_60_1","first-page":"139","volume-title":"TACAS","author":"Piskac R.","year":"2014","unstructured":"R. Piskac , T. Wies , and D. Zufferey . Grasshopper - complete heap verification with mixed specifications. In Tools and Algorithms for the Construction and Analysis of Systems , TACAS , pages 124\u2013 139 , 2014 . R. Piskac, T. Wies, and D. Zufferey. Grasshopper - complete heap verification with mixed specifications. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pages 124\u2013139, 2014."},{"key":"e_1_3_2_1_61_1","volume-title":"EPFL","author":"Prokopec A.","year":"2014","unstructured":"A. Prokopec . Data Structures and Algorithms for Data-Parallel Computing in a Managed Runtime. PhD thesis , EPFL , 2014 . A. Prokopec. Data Structures and Algorithms for Data-Parallel Computing in a Managed Runtime. PhD thesis, EPFL, 2014."},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29778-1_16"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292552"},{"key":"e_1_3_2_1_66_1","unstructured":"D. Sands. Calculi for Time Anlaysis of Functional Programs. PhD thesis Imperial College University of London 1990.  D. Sands. Calculi for Time Anlaysis of Functional Programs. PhD thesis Imperial College University of London 1990."},{"key":"e_1_3_2_1_67_1","first-page":"376","volume-title":"European Symposium on Programming, ESOP","author":"Sands D.","year":"1990","unstructured":"D. Sands . Complexity analysis for a lazy higher-order language . In European Symposium on Programming, ESOP , pages 361\u2013 376 , 1990 . D. Sands. Complexity analysis for a lazy higher-order language. In European Symposium on Programming, ESOP, pages 361\u2013376, 1990."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364575"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041575"},{"key":"e_1_3_2_1_72_1","volume-title":"A library for manipulating infinite lists. https:\/\/hackage.haskell.org\/package\/Stream-0.4.7.2\/ docs\/Data-Stream.html","author":"Swierstra W.","year":"2015","unstructured":"W. Swierstra . Stream : A library for manipulating infinite lists. https:\/\/hackage.haskell.org\/package\/Stream-0.4.7.2\/ docs\/Data-Stream.html . 2015 . W. Swierstra. Stream: A library for manipulating infinite lists. https:\/\/hackage.haskell.org\/package\/Stream-0.4.7.2\/ docs\/Data-Stream.html. 2015."},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384655"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_32"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1967.1054010"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2774975.2774978"},{"key":"e_1_3_2_1_78_1","volume-title":"EPFL-REPORT-222712. Technical report","author":"Voirol N.","year":"2016","unstructured":"N. Voirol and V. Kuncak . Automating verification of functional programs with quantified invariants , EPFL-REPORT-222712. Technical report , EPFL , 2016 . N. Voirol and V. Kuncak. Automating verification of functional programs with quantified invariants, EPFL-REPORT-222712. Technical report, EPFL, 2016."},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103767"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041574"},{"key":"e_1_3_2_1_85_1","unstructured":"Introduction Language and Semantics Generating Model Programs Model Verification and Inference Evaluation Related Work  Introduction Language and Semantics Generating Model Programs Model Verification and Inference Evaluation Related Work"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009874","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:05:33Z","timestamp":1750259133000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":84,"alternative-id":["10.1145\/3009837.3009874","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009874","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009874","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}