{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:58Z","timestamp":1775873518329,"version":"3.50.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-18-C-0092"],"award-info":[{"award-number":["FA8750-18-C-0092"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1801369, 1845514,1812876,1814358,2007784"],"award-info":[{"award-number":["1801369, 1845514,1812876,1814358,2007784"]}],"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":[[2020,8,2]]},"abstract":"<jats:p>This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility \u2013 automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program\u2019s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof.<\/jats:p>","DOI":"10.1145\/3408988","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T13:48:02Z","timestamp":1596462482000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Liquid resource types"],"prefix":"10.1145","volume":"4","author":[{"given":"Tristan","family":"Knoth","sequence":"first","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Di","family":"Wang","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Reynolds","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"E. Albert P. Arenas S. Genaim and G. Puebla. 2011. Closed-Form Upper Bounds in Static Cost Analysis. J. Automated Reasoning 46 (February 2011 ). Issue 2.  E. Albert P. Arenas S. Genaim and G. Puebla. 2011. Closed-Form Upper Bounds in Static Cost Analysis. J. Automated Reasoning 46 (February 2011 ). Issue 2.","DOI":"10.1007\/s10817-010-9174-1"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"E. Albert J. C. Fern\u00e1ndez and G. Rom\u00e1n-D\u00edez. 2015. Non-cumulative Resource Analysis. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'15).  E. Albert J. C. Fern\u00e1ndez and G. Rom\u00e1n-D\u00edez. 2015. Non-cumulative Resource Analysis. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'15).","DOI":"10.1007\/978-3-662-46681-0_6"},{"key":"e_1_2_2_3_1","volume-title":"FMCAD 2013","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur , Rastislav Bod\u00edk , Garvit Juniwal , Milo M. K. Martin , Mukund Raghothaman , Sanjit A. Seshia , Rishabh Singh , Armando Solar-Lezama , Emina Torlak , and Abhishek Udupa . 2013 . Syntax-guided synthesis. In Formal Methods in Computer-Aided Design , FMCAD 2013 , Portland, OR, USA , October 20-23, 2013. 1-8. http:\/\/ieeexplore.ieee.org\/document\/ 6679385\/ Rajeev Alur, Rastislav Bod\u00edk, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. 1-8. http:\/\/ieeexplore.ieee.org\/document\/ 6679385\/"},{"key":"e_1_2_2_4_1","volume-title":"Sorting Morphisms","author":"Augusteijn Lex","unstructured":"Lex Augusteijn . 1999. Sorting Morphisms . In Advanced Functional Programming, S. Doaitse Swierstra, Jos\u00e9 N. Oliveira, and Pedro R. Henriques (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 1-27. Lex Augusteijn. 1999. Sorting Morphisms. In Advanced Functional Programming, S. Doaitse Swierstra, Jos\u00e9 N. Oliveira, and Pedro R. Henriques (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1-27."},{"key":"e_1_2_2_5_1","volume-title":"Int. Conf. on Rewriting Techniques and Applications (RTA'13)","author":"Avanzini M.","unstructured":"M. Avanzini and G. Moser . 2013. A Combination Framework for Complexity . In Int. Conf. on Rewriting Techniques and Applications (RTA'13) . M. Avanzini and G. Moser. 2013. A Combination Framework for Complexity. In Int. Conf. on Rewriting Techniques and Applications (RTA'13)."},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"M. Brockschmidt F. Emmes S. Falke C. Fuhs and J. Giesl. 2014. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'14).  M. Brockschmidt F. Emmes S. Falke C. Fuhs and J. Giesl. 2014. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Algs. for the Construct. and Anal. of Syst. (TACAS'14).","DOI":"10.1007\/978-3-642-54862-8_10"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"E. \u00c7i\u00e7ek G. Barthe M. Gaboardi D. Garg and J. Hofmann. 2017. Relational Cost Analysis. In Princ. of Prog. Lang. (POPL'17).  E. \u00c7i\u00e7ek G. Barthe M. Gaboardi D. Garg and J. Hofmann. 2017. Relational Cost Analysis. In Princ. of Prog. Lang. (POPL'17).","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314603"},{"key":"e_1_2_2_10_1","first-page":"133","volume-title":"Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In 35th ACM Symp. on Principles Prog. Langs. (POPL'08)","author":"Danielsson Nils Anders","year":"2008","unstructured":"Nils Anders Danielsson . 2008 . Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In 35th ACM Symp. on Principles Prog. Langs. (POPL'08) . 133 - 144 . Nils Anders Danielsson. 2008. Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. In 35th ACM Symp. on Principles Prog. Langs. (POPL'08). 133-144."},{"key":"e_1_2_2_11_1","volume-title":"Denotational Cost Semantics for Functional Languages with Inductive Types. In Int. Conf. on Functional Programming (ICFP'15)","author":"Danner N.","unstructured":"N. Danner , D. R. Licata , and R. Ramyaa . 2015 . Denotational Cost Semantics for Functional Languages with Inductive Types. In Int. Conf. on Functional Programming (ICFP'15) . N. Danner, D. R. Licata, and R. Ramyaa. 2015. Denotational Cost Semantics for Functional Languages with Inductive Types. In Int. Conf. on Functional Programming (ICFP'15)."},{"key":"e_1_2_2_13_1","doi-asserted-by":"crossref","unstructured":"T. Freeman and F. Pfenning. 1991. Refinement Types for ML. In Prog. Lang. Design and Impl. (PLDI'91).  T. Freeman and F. Pfenning. 1991. Refinement Types for ML. In Prog. Lang. Design and Impl. (PLDI'91).","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_2_2_15_1","volume-title":"Scott","author":"Girard Jean-Yves","year":"1992","unstructured":"Jean-Yves Girard , Andre Scedrov , and Philip J . Scott . 1992 . Bounded Linear Logic: A Modular Approach to Polynomial-Time Computability. Theor. Comput. Sci . 97, 1 ( 1992 ), 1-66. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded Linear Logic: A Modular Approach to Polynomial-Time Computability. Theor. Comput. Sci. 97, 1 ( 1992 ), 1-66."},{"key":"e_1_2_2_16_1","first-page":"375","volume-title":"Control-Flow Refinement and Progress Invariants for Bound Analysis. In Conf. on Prog. Lang. Design and Impl. (PLDI'09)","author":"Gulwani Sumit","year":"2009","unstructured":"Sumit Gulwani , Sagar Jain , and Eric Koskinen . 2009 a. Control-Flow Refinement and Progress Invariants for Bound Analysis. In Conf. on Prog. Lang. Design and Impl. (PLDI'09) . 375 - 385 . Sumit Gulwani, Sagar Jain, and Eric Koskinen. 2009a. Control-Flow Refinement and Progress Invariants for Bound Analysis. In Conf. on Prog. Lang. Design and Impl. (PLDI'09). 375-385."},{"key":"e_1_2_2_17_1","volume-title":"SPEED: Precise and Eficient Static Estimation of Program Computational Complexity. In Princ. of Prog. Lang. (POPL'09).","author":"Gulwani S.","year":"2009","unstructured":"S. Gulwani , K. K. Mehra , and T. M. Chilimbi . 2009 b. SPEED: Precise and Eficient Static Estimation of Program Computational Complexity. In Princ. of Prog. Lang. (POPL'09). S. Gulwani, K. K. Mehra, and T. M. Chilimbi. 2009b. SPEED: Precise and Eficient Static Estimation of Program Computational Complexity. In Princ. of Prog. Lang. (POPL'09)."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371092"},{"key":"e_1_2_2_19_1","volume-title":"Practical Foundations for Programming Languages","author":"Harper R.","unstructured":"R. Harper . 2016. Practical Foundations for Programming Languages . Cambridge University Press . R. Harper. 2016. Practical Foundations for Programming Languages. Cambridge University Press."},{"key":"e_1_2_2_20_1","first-page":"357","volume-title":"Multivariate Amortized Resource Analysis. In 38th Symp. on Principles of Prog. Langs. (POPL'11)","author":"Hofmann Jan","year":"2011","unstructured":"Jan Hofmann , Klaus Aehlig , and Martin Hofmann . 2011 a. Multivariate Amortized Resource Analysis. In 38th Symp. on Principles of Prog. Langs. (POPL'11) . 357 - 370 . Jan Hofmann, Klaus Aehlig, and Martin Hofmann. 2011a. Multivariate Amortized Resource Analysis. In 38th Symp. on Principles of Prog. Langs. (POPL'11). 357-370."},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"J. Hofmann K. Aehlig and M. Hofmann. 2011b. Multivariate Amortized Resource Analysis. In Princ. of Prog. Lang. (POPL'11).  J. Hofmann K. Aehlig and M. Hofmann. 2011b. Multivariate Amortized Resource Analysis. In Princ. of Prog. Lang. (POPL'11).","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"J. Hofmann A. Das and S.-C. Weng. 2017. Towards Automatic Resource Bound Analysis for OCaml. In Princ. of Prog. Lang. (POPL'17).  J. Hofmann A. Das and S.-C. Weng. 2017. Towards Automatic Resource Bound Analysis for OCaml. In Princ. of Prog. Lang. (POPL'17).","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_2_2_23_1","volume-title":"Amortized Resource Analysis with Polynomial Potential. In European Symp. on Programming (ESOP'10)","author":"Hofmann J.","unstructured":"J. Hofmann and M. Hofmann . 2010a . Amortized Resource Analysis with Polynomial Potential. In European Symp. on Programming (ESOP'10) . J. Hofmann and M. Hofmann. 2010a. Amortized Resource Analysis with Polynomial Potential. In European Symp. on Programming (ESOP'10)."},{"key":"e_1_2_2_24_1","first-page":"287","volume-title":"Amortized Resource Analysis with Polynomial Potential-A Static Inference of Polynomial Bounds for Functional Programs. In In Proceedings of the 19th European Symposium on Programming (ESOP'10)","volume":"6012","author":"Hofmann Jan","year":"2010","unstructured":"Jan Hofmann and Martin Hofmann . 2010 b. Amortized Resource Analysis with Polynomial Potential-A Static Inference of Polynomial Bounds for Functional Programs. In In Proceedings of the 19th European Symposium on Programming (ESOP'10) (Lecture Notes in Computer Science) , Vol. 6012 . Springer, 287 - 306 . Jan Hofmann and Martin Hofmann. 2010b. Amortized Resource Analysis with Polynomial Potential-A Static Inference of Polynomial Bounds for Functional Programs. In In Proceedings of the 19th European Symposium on Programming (ESOP'10) (Lecture Notes in Computer Science), Vol. 6012. Springer, 287-306."},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"M. Hofmann and S. Jost. 2003. Static Prediction of Heap Space Usage for First-Order Functional Programs. In Princ. of Prog. Lang. (POPL'03).  M. Hofmann and S. Jost. 2003. Static Prediction of Heap Space Usage for First-Order Functional Programs. In Princ. of Prog. Lang. (POPL'03).","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_2_26_1","volume-title":"Multivariate Amortised Resource Analysis for Term Rewrite Systems. In Int. Conf. on Typed Lambda Calculi and Applications (TLCA'15)","author":"Hofmann M.","unstructured":"M. Hofmann and G. Moser . 2015 . Multivariate Amortised Resource Analysis for Term Rewrite Systems. In Int. Conf. on Typed Lambda Calculi and Applications (TLCA'15) . M. Hofmann and G. Moser. 2015. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In Int. Conf. on Typed Lambda Calculi and Applications (TLCA'15)."},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"S. Jost K. Hammond H.-W. Loidl and M. Hofmann. 2010. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In Princ. of Prog. Lang. (POPL'10).  S. Jost K. Hammond H.-W. Loidl and M. Hofmann. 2010. Static Determination of Quantitative Resource Usage for Higher-Order Programs. In Princ. of Prog. Lang. (POPL'10).","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Z. Kincaid J. Breck A. F. Boroujeni and T. Reps. 2017. Compositional Recurrence Analysis Revisited. In Prog. Lang. Design and Impl. (PLDI'17).  Z. Kincaid J. Breck A. F. Boroujeni and T. Reps. 2017. Compositional Recurrence Analysis Revisited. In Prog. Lang. Design and Impl. (PLDI'17).","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_2_2_29_1","unstructured":"Z. Kincaid J. Cyphert J. Breck and T. Reps. 2019. Non-linear Reasoning for Invariant Synthesis. In Princ. of Prog. Lang. (POPL'19).  Z. Kincaid J. Cyphert J. Breck and T. Reps. 2019. Non-linear Reasoning for Invariant Synthesis. In Princ. of Prog. Lang. (POPL'19)."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314602"},{"key":"e_1_2_2_31_1","volume-title":"Liquid Resource Types (Extended Version). ( 2020 ). arXiv:cs.PL\/","author":"Knoth Tristan","year":"2006","unstructured":"Tristan Knoth , Di Wang , Adam Reynolds , Jan Hofmann , and Nadia Polikarpova . 2020. Liquid Resource Types (Extended Version). ( 2020 ). arXiv:cs.PL\/ 2006 .16233 Tristan Knoth, Di Wang, Adam Reynolds, Jan Hofmann, and Nadia Polikarpova. 2020. Liquid Resource Types (Extended Version). ( 2020 ). arXiv:cs.PL\/ 2006.16233"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"U. D. Lago and M. Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In Logic in Computer Science (LICS'11).  U. D. Lago and M. Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In Logic in Computer Science (LICS'11).","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"L. Noschinski F. Emmes and J. Giesl. 2013. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. J. Automated Reasoning 51 ( June 2013 ). Issue 1.  L. Noschinski F. Emmes and J. Giesl. 2013. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. J. Automated Reasoning 51 ( June 2013 ). Issue 1.","DOI":"10.1007\/s10817-013-9277-6"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"e_1_2_2_38_1","doi-asserted-by":"crossref","unstructured":"Andrew Reynolds Viktor Kuncak Cesare Tinelli Clark W. Barrett and Morgan Deters. 2019. Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55 2 ( 2019 ) 73-102.  Andrew Reynolds Viktor Kuncak Cesare Tinelli Clark W. Barrett and Morgan Deters. 2019. Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55 2 ( 2019 ) 73-102.","DOI":"10.1007\/s10703-017-0270-2"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_59"},{"key":"e_1_2_2_40_1","unstructured":"Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid types. In PLDI.  Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid types. In PLDI."},{"key":"e_1_2_2_41_1","doi-asserted-by":"crossref","unstructured":"A. Sabry and M. Felleisen. 1992. Reasoning about Programs in Continuation-Passing Style. In LISP and Functional Programming (LFP'92).  A. Sabry and M. Felleisen. 1992. Reasoning about Programs in Continuation-Passing Style. In LISP and Functional Programming (LFP'92).","DOI":"10.1145\/141471.141563"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_2_2_43_1","volume-title":"Saraswat","author":"Solar-Lezama Armando","year":"2006","unstructured":"Armando Solar-Lezama , Liviu Tancau , Rastislav Bod\u00edk , Sanjit A. Seshia , and Vijay A . Saraswat . 2006 . Combinatorial sketching for finite programs. In ASPLOS. Armando Solar-Lezama, Liviu Tancau, Rastislav Bod\u00edk, Sanjit A. Seshia, and Vijay A. Saraswat. 2006. Combinatorial sketching for finite programs. In ASPLOS."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_45_1","series-title":"SIAM J. Algebraic Discrete Methods 6 (","volume-title":"Amortized Computational Complexity","author":"Tarjan R. E.","year":"1985","unstructured":"R. E. Tarjan . 1985. Amortized Computational Complexity . SIAM J. Algebraic Discrete Methods 6 ( August 1985 ). Issue 2. R. E. Tarjan. 1985. Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods 6 ( August 1985 ). Issue 2."},{"key":"e_1_2_2_46_1","volume-title":"Patrick Maxim Rondon, and Ranjit Jhala","author":"Vazou Niki","year":"2013","unstructured":"Niki Vazou , Patrick Maxim Rondon, and Ranjit Jhala . 2013 . Abstract Refinement Types. In ESOP. Niki Vazou, Patrick Maxim Rondon, and Ranjit Jhala. 2013. Abstract Refinement Types. In ESOP."},{"key":"e_1_2_2_47_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker D.","unstructured":"D. Walker . 2002. Substructural Type Systems . In Advanced Topics in Types and Programming Languages . MIT Press . D. Walker. 2002. Substructural Type Systems. In Advanced Topics in Types and Programming Languages. MIT Press."},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","unstructured":"P. Wang D. Wang and A. Chlipala. 2017. TiML: A Functional Language for Practical Complexity Analysis with Invariants. In Object-Oriented Prog. Syst. Lang. and Applications (OOPSLA'17).  P. Wang D. Wang and A. Chlipala. 2017. TiML: A Functional Language for Practical Complexity Analysis with Invariants. In Object-Oriented Prog. Syst. Lang. and Applications (OOPSLA'17).","DOI":"10.1145\/3133903"},{"key":"e_1_2_2_49_1","doi-asserted-by":"crossref","unstructured":"Ben Wegbreit. 1975. Mechanical Program Analysis. Commun. ACM 18 9 ( 1975 ) 528-539.  Ben Wegbreit. 1975. Mechanical Program Analysis. Commun. ACM 18 9 ( 1975 ) 528-539.","DOI":"10.1145\/361002.361016"},{"key":"e_1_2_2_50_1","volume-title":"Bound Analysis of Imperative Programs with the Size-change Abstraction. In Static Analysis Symp. (SAS'11)","author":"Zuleger F.","unstructured":"F. Zuleger , M. Sinn , S. Gulwani , and H. Veith . 2011 . Bound Analysis of Imperative Programs with the Size-change Abstraction. In Static Analysis Symp. (SAS'11) . F. Zuleger, M. Sinn, S. Gulwani, and H. Veith. 2011. Bound Analysis of Imperative Programs with the Size-change Abstraction. In Static Analysis Symp. (SAS'11)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408988","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408988","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408988","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:59Z","timestamp":1750193279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408988"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":49,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3408988"],"URL":"https:\/\/doi.org\/10.1145\/3408988","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}