{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T18:51:13Z","timestamp":1777488673383,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T00:00:00Z","timestamp":1591833600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100015089","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2889,N00014-19-1-2318"],"award-info":[{"award-number":["N00014-17-1-2889,N00014-19-1-2318"]}],"id":[{"id":"10.13039\/100015089","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,11]]},"DOI":"10.1145\/3385412.3386035","type":"proceedings-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T01:40:10Z","timestamp":1591494010000},"page":"688-702","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Templates and recurrences: better together"],"prefix":"10.1145","author":[{"given":"Jason","family":"Breck","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Cyphert","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zachary","family":"Kincaid","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"E. Albert P. Arenas and S. Genaim. 2011. Closed-Form Upper Bounds in Static Cost Analysis. J. Autom. Reasoning (2011).","DOI":"10.1007\/s10817-010-9174-1"},{"key":"e_1_3_2_1_2_1","volume-title":"PUBS: A Practical Upper Bound Solver. https:\/\/costa.fdi.ucm.es\/pubs\/examples.php","author":"Albert E.","year":"2019","unstructured":"E. Albert, P. Arenas, S. Genaim, and G. Puebla. 2019. PUBS: A Practical Upper Bound Solver. https:\/\/costa.fdi.ucm.es\/pubs\/examples.php"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"E. Albert S. Genaim and A. Masud. 2013. On the Inference of Resource Usage Upper and Lower Bounds. In ACM. Trans. Comput. Logic.","DOI":"10.1145\/2499937.2499943"},{"key":"e_1_3_2_1_4_1","unstructured":"J. Breck J. Cyphert Z. Kincaid and T. Reps. 2020. CHORA repository. https:\/\/github.com\/jbreck\/duet-jbreck"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"J. Breck J. Cyphert Z. Kincaid and T. Reps. 2020. Templates and Recurrences: Better Together. (2020). arXiv: 2003.13515 [cs.PL]","DOI":"10.1145\/3385412.3386035"},{"key":"e_1_3_2_1_6_1","volume":"201","author":"Brockschmidt M.","unstructured":"M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. 2016. Analyzing Runtime and Size Complexity of Integer Programs. ACM Trans. Program. Lang. Syst. (2016).","journal-title":"J. Giesl."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"David Cachera Thomas Jensen Arnaud Jobin and Florent Kirchner. 2012. Inference of Polynomial Invariants for Imperative Programs: A Farewell to Gr\u00f6bner Bases. In SAS. 58\u201374.","DOI":"10.1007\/978-3-642-33125-1_7"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Q. Carbonneaux J. Hoffmann and Z. Shao. 2015. Compositional Certified Resource Bounds. In PLDI.","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"K. Chatterjee H. Fu and A. Goharshady. 2019. Non-polynomial Worst-Case Analysis of Recursive Programs. TOPLAS. (2019).","DOI":"10.1145\/3339984"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"M.A. Col\u00f3n S. Sankaranarayanan and H. Sipma. 2003. Linear Invariant Generation Using Non-Linear Constraint Solving. In CAV.","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"S. de Oliveira S. Bensalem and V. Prevosto. 2016. Polynomial Invariants by Linear Algebra. In ATVA. 479\u2013494.","DOI":"10.1007\/978-3-319-46520-3_30"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"D. Dietsch M. Greitschus M. Heizmann J. Hoenicke A. Nutz A. Podelski C. Schilling and T. Schindler. 2018. Ultimate Taipan with Dynamic Block Encoding - (Competition Contribution). In TACAS.","DOI":"10.1007\/978-3-319-89963-3_31"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"A. Farzan and Z. Kincaid. 2015. Compositional Recurrence Analysis. In FMCAD.","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"M. Heizmann J. Christ D. Dietsch E. Ermis J. Hoenicke M. Lindenmann A. Nutz C. Schilling and A. Podelski. 2013. Ultimate Automizer with SMTInterpol (Competition Contribution). In TACAS.","DOI":"10.1007\/978-3-642-36742-7_53"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"J. Hoffmann K. Aehlig and M. Hofmann. 2012. Resource Aware ML. In CAV.","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"A. Humenberger M. Jaroschek and L. Kovacs. 2017. Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences. In ISSAC.","DOI":"10.1145\/3087604.3087623"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"A. Humenberger M. Jaroschek and L. Kov\u00e1cs. 2018. Invariant Generation for Multi-Path Loops with Polynomial Assignments. In VMCAI. 226\u2013246.","DOI":"10.1007\/978-3-319-73721-8_11"},{"key":"e_1_3_2_1_20_1","volume":"201","author":"Kahn D.","unstructured":"D. Kahn and J. Hoffmann. 2019. Exponential Automatic Amortized Resource Analysis. Technical Report. Carnegie Mellon University.","journal-title":"J. Hoffmann."},{"key":"e_1_3_2_1_21_1","unstructured":"Deepak Kapur. 2004. Automatically Generating Loop Invariants Using Quantifier Elimination. In ACA."},{"key":"e_1_3_2_1_22_1","volume-title":"The Concrete Tetrahedron: symbolic sums, recurrence equations, generating functions, asymptotic estimates","author":"Kauers Manuel","unstructured":"Manuel Kauers and Peter Paule. 2011. The Concrete Tetrahedron: symbolic sums, recurrence equations, generating functions, asymptotic estimates. Springer Science & Business Media."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Z. Kincaid J. Breck J. Cyphert and T. Reps. 2019. Closed Forms for Numerical Loops. In POPL.","DOI":"10.1145\/3290368"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Z. Kincaid J. Breck A. Forouhi Boroujeni and T. Reps. 2017. Compositional Recurrence Analysis Revisited. In PLDI.","DOI":"10.1145\/3062341.3062373"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Z. Kincaid J. Cyphert J. Breck and T. Reps. 2018. Non-Linear Reasoning for Invariant Synthesis. PACMPL 2(POPL) (2018) 54:1\u201354:33.","DOI":"10.1145\/3158142"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Kensuke Kojima Minoru Kinoshita and Kohei Suenaga. 2016. Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis. In SAS.","DOI":"10.1007\/978-3-662-53413-7_14"},{"key":"e_1_3_2_1_27_1","unstructured":"L. Kov\u00e1cs. 2008. Reasoning Algebraically About P-Solvable Loops. In TACAS."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Pritom Rajkhowa and Fangzhen Lin. 2017. VIAP - Automated System for Verifying Integer Assignment Programs with Loops. In SYNASC.","DOI":"10.1109\/SYNASC.2017.00032"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"T. Reps E. Turetsky and P. Prabhu. 2017. Newtonian Program Analysis via Tensor Product. TOPLAS. 39 2 9:1\u20139:72.","DOI":"10.1145\/3024084"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"E. Rodr\u00edguez-Carbonell and D. Kapur. 2004. Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations. In ISSAC. 266\u2013 273.","DOI":"10.1145\/1005285.1005324"},{"key":"e_1_3_2_1_31_1","unstructured":"S. Sankaranarayanan H. Sipma and Z. Manna. 2004. Constraint-Based Linear-Relations Analysis. In SAS. Templates and Recurrences: Better Together PLDI \u201920 June 15\u201320 2020 London UK"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Sriram Sankaranarayanan Henny B. Sipma and Zohar Manna. 2004. Non-linear Loop Invariant Generation Using Gr\u00f6Bner Bases. In POPL.","DOI":"10.1145\/964001.964028"},{"key":"e_1_3_2_1_33_1","volume-title":"Mechanical program analysis. Commun. ACM","author":"Wegbreit Ben","year":"1975","unstructured":"Ben Wegbreit. 1975. Mechanical program analysis. Commun. ACM (1975)."}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3386035","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3386035","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3386035","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:50Z","timestamp":1750199930000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3386035"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,11]]},"references-count":32,"alternative-id":["10.1145\/3385412.3386035","10.1145\/3385412"],"URL":"https:\/\/doi.org\/10.1145\/3385412.3386035","relation":{},"subject":[],"published":{"date-parts":[[2020,6,11]]},"assertion":[{"value":"2020-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}