{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:30:39Z","timestamp":1750221039908,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["NI 491\/16-1"],"award-info":[{"award-number":["NI 491\/16-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294090","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"27-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Verified solving and asymptotics of linear recurrences"],"prefix":"10.1145","author":[{"given":"Manuel","family":"Eberl","sequence":"first","affiliation":[{"name":"TU Munich, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"R. Bagnara A. Zaccagnini and T. Zolo. 2003. The Automatic Solution of Recurrence Relations. I. Linear Recurrences of Finite Order with Constant Coefficients . Quaderno 334. Dipartimento di Matematica Universit\u00e0 di Parma Italy. Available at http:\/\/www.cs.unipr.it\/Publications\/ .  R. Bagnara A. Zaccagnini and T. Zolo. 2003. The Automatic Solution of Recurrence Relations. I. Linear Recurrences of Finite Order with Constant Coefficients . Quaderno 334. Dipartimento di Matematica Universit\u00e0 di Parma Italy. Available at http:\/\/www.cs.unipr.it\/Publications\/ ."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Lukas Bulwahn. 2012. The New Quickcheck for Isabelle. Springer Berlin Heidelberg Berlin Heidelberg 92\u2013108.  Lukas Bulwahn. 2012. The New Quickcheck for Isabelle. Springer Berlin Heidelberg Berlin Heidelberg 92\u2013108.","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9195-9"},{"key":"e_1_3_2_1_4_1","unstructured":"Manuel Eberl. 2017. Linear Recurrences. Archive of Formal Proofs (Oct. 2017). http:\/\/isa-afp.org\/entries\/Linear_Recurrences.html Formal proof development.  Manuel Eberl. 2017. Linear Recurrences. Archive of Formal Proofs (Oct. 2017). http:\/\/isa-afp.org\/entries\/Linear_Recurrences.html Formal proof development."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Philippe Flajolet and Robert Sedgewick. 2009. Analytic Combinatorics (1 ed.). Cambridge University Press New York NY USA.   Philippe Flajolet and Robert Sedgewick. 2009. Analytic Combinatorics (1 ed.). Cambridge University Press New York NY USA.","DOI":"10.1017\/CBO9780511801655"},{"key":"e_1_3_2_1_7_1","volume-title":"Concrete Mathematics: A Foundation for Computer Science","author":"Graham Ronald L.","year":"1994","edition":"2"},{"key":"e_1_3_2_1_8_1","unstructured":"Ond\u0159ej Kun\u010dar. 2016. Types Abstraction and Parametric Polymorphism in Higher-Order Logic . Ph.D. Dissertation. https:\/\/www21.in.tum.de\/ ~kuncar\/documents\/kuncar-phdthesis.pdf  Ond\u0159ej Kun\u010dar. 2016. Types Abstraction and Parametric Polymorphism in Higher-Order Logic . Ph.D. Dissertation. https:\/\/www21.in.tum.de\/ ~kuncar\/documents\/kuncar-phdthesis.pdf"},{"key":"e_1_3_2_1_9_1","unstructured":"Wenda Li. 2017. Count the Number of Complex Roots. Archive of Formal Proofs (Oct. 2017). http:\/\/isa-afp.org\/entries\/Count_Complex_ Roots.html Formal proof development.  Wenda Li. 2017. Count the Number of Complex Roots. Archive of Formal Proofs (Oct. 2017). http:\/\/isa-afp.org\/entries\/Count_Complex_ Roots.html Formal proof development."},{"key":"e_1_3_2_1_10_1","unstructured":"Wenda Li and Lawrence C. Paulson. 2018. Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle\/HOL. CoRR abs\/1804.03922 (2018). http:\/\/arxiv.org\/abs\/1804. 03922  Wenda Li and Lawrence C. Paulson. 2018. Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle\/HOL. CoRR abs\/1804.03922 (2018). http:\/\/arxiv.org\/abs\/1804. 03922"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2766189.2766191"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Ren\u00e9 Thiemann and Akihisa Yamada. 2015. Algebraic Numbers in Isabelle\/HOL. Archive of Formal Proofs (Dec. 2015). http:\/\/isa-afp.org\/ entries\/Algebraic_Numbers.html Formal proof development.  Ren\u00e9 Thiemann and Akihisa Yamada. 2015. Algebraic Numbers in Isabelle\/HOL. Archive of Formal Proofs (Dec. 2015). http:\/\/isa-afp.org\/ entries\/Algebraic_Numbers.html Formal proof development.","DOI":"10.1007\/978-3-319-43144-4_24"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Ren\u00e9 Thiemann and Akihisa Yamada. 2016. Algebraic numbers in Isabelle\/HOL . Springer International Publishing Cham 391\u2013408.  Ren\u00e9 Thiemann and Akihisa Yamada. 2016. Algebraic numbers in Isabelle\/HOL . Springer International Publishing Cham 391\u2013408.","DOI":"10.1007\/978-3-319-43144-4_24"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854073"},{"key":"e_1_3_2_1_16_1","unstructured":"Ren\u00e9 Thiemann and Akihisa Yamada. 2016. Polynomial Factorization. Archive of Formal Proofs (Jan. 2016). http:\/\/isa-afp.org\/entries\/ Polynomial_Factorization.html Formal proof development.  Ren\u00e9 Thiemann and Akihisa Yamada. 2016. Polynomial Factorization. Archive of Formal Proofs (Jan. 2016). http:\/\/isa-afp.org\/entries\/ Polynomial_Factorization.html Formal proof development."},{"key":"e_1_3_2_1_17_1","unstructured":"Bohua Zhan and Maximilian P. L. Haslbeck. 2018. Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. CoRR abs\/1802.01336 (2018). http:\/\/arxiv.org\/abs\/1802.01336  Bohua Zhan and Maximilian P. L. Haslbeck. 2018. Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle. CoRR abs\/1802.01336 (2018). http:\/\/arxiv.org\/abs\/1802.01336"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Cascais Portugal","acronym":"CPP '19"},"container-title":["Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294090","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:49Z","timestamp":1750207429000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294090"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":16,"alternative-id":["10.1145\/3293880.3294090","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294090","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}