{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:05:07Z","timestamp":1750089907779,"version":"3.37.3"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2020,6,1]],"date-time":"2020-06-01T00:00:00Z","timestamp":1590969600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,6,9]],"date-time":"2020-06-09T00:00:00Z","timestamp":1591660800000},"content-version":"vor","delay-in-days":8,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["Y757","Y757"],"award-info":[{"award-number":["Y757","Y757"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["Y757","Y757"],"award-info":[{"award-number":["Y757","Y757"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["Y757"],"award-info":[{"award-number":["Y757"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100010198","name":"Ministerio de Econom\u00eda, Industria y Competitividad","doi-asserted-by":"crossref","award":["MTM2017-88804-P"],"award-info":[{"award-number":["MTM2017-88804-P"]}],"id":[{"id":"10.13039\/501100010198","id-type":"DOI","asserted-by":"crossref"}]},{"name":"NWO","award":["VICI 639.023.710"],"award-info":[{"award-number":["VICI 639.023.710"]}]},{"DOI":"10.13039\/501100002241","name":"Japan Science and Technology Agency","doi-asserted-by":"crossref","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has applications in number theory, computer algebra and cryptography. In this paper, we provide an implementation of the LLL algorithm. Both its soundness and its polynomial running-time have been verified using Isabelle\/HOL. Our implementation is nearly as fast as an implementation in a commercial computer algebra system, and its efficiency can be further increased by connecting it with fast untrusted lattice reduction algorithms and certifying their output. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.\n<\/jats:p>","DOI":"10.1007\/s10817-020-09552-1","type":"journal-article","created":{"date-parts":[[2020,6,9]],"date-time":"2020-06-09T17:03:08Z","timestamp":1591722188000},"page":"827-856","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle\/HOL"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0323-8829","authenticated-orcid":false,"given":"Ren\u00e9","family":"Thiemann","sequence":"first","affiliation":[]},{"given":"Ralph","family":"Bottesch","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5173-128X","authenticated-orcid":false,"given":"Jose","family":"Divas\u00f3n","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9900-5746","authenticated-orcid":false,"given":"Max W.","family":"Haslbeck","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6590-6220","authenticated-orcid":false,"given":"Sebastiaan J. C.","family":"Joosten","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8872-2240","authenticated-orcid":false,"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,6,9]]},"reference":[{"issue":"2","key":"9552_CR1","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014)","journal-title":"J. Autom. Reason."},{"key":"9552_CR2","unstructured":"Bottesch, R., Divas\u00f3n, J., Haslbeck, M., Joosten, S.J.C., Thiemann, R., Yamada, A.: A verified LLL algorithm. In: Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/LLL_Basis_Reduction.html, Formal proof development"},{"key":"9552_CR3","unstructured":"Bottesch, R., Haslbeck, M.W., Thiemann, R.: A verified efficient implementation of the LLL basis reduction algorithm. In: LPAR\u00a02018, volume\u00a057 of EPiC Series in Computing, pp. 64\u2013180 (2018)"},{"key":"9552_CR4","doi-asserted-by":"crossref","unstructured":"Cohen, C.: Construction of real algebraic numbers in Coq. In: ITP\u00a02012, volume 7406 of LNCS, pp. 7\u201382 (2012)","DOI":"10.1007\/978-3-642-32347-8_6"},{"key":"9552_CR5","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Factoring univariate integral polynomials in polynomial average time. In: EUROSAM\u00a01979, volume\u00a072 of LNCS (1979)","DOI":"10.1007\/3-540-09519-5_84"},{"key":"9552_CR6","doi-asserted-by":"crossref","unstructured":"Divas\u00f3n, J., Joosten, S.J.C., Kun\u010dar, O., Thiemann, R., Yamada, A.: Efficient certification of complexity proofs: formalizing the Perron\u2013Frobenius theorem (invited talk paper). In: CPP 2018, pp. 2\u201313. ACM (2018)","DOI":"10.1145\/3176245.3167103"},{"key":"9552_CR7","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1007\/s10817-019-09526-y","volume":"64","author":"J Divas\u00f3n","year":"2020","unstructured":"Divas\u00f3n, J., Joosten, S., Thiemann, R., Yamada, A.: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. J. Autom. Reason. 64, 699\u2013735 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09526-y","journal-title":"J. Autom. Reason."},{"key":"9552_CR8","doi-asserted-by":"crossref","unstructured":"Divas\u00f3n, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A formalization of the LLL basis reduction algorithm. In: ITP 2018, volume 10895 of LNCS, pp. 160\u2013177 (2018)","DOI":"10.1007\/978-3-319-94821-8_10"},{"key":"9552_CR9","unstructured":"Divas\u00f3n, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A verified factorization algorithm for integer polynomials with polynomial complexity. In: Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/LLL_Factorization.html, Formal proof development"},{"key":"9552_CR10","doi-asserted-by":"crossref","unstructured":"Eberl, M.: Verified solving and asymptotics of linear recurrences. In: CPP\u00a02019, pp. 27\u201337. ACM (2019)","DOI":"10.1145\/3293880.3294090"},{"key":"9552_CR11","doi-asserted-by":"crossref","unstructured":"Eberl, M., Haslbeck, M.W., Nipkow, T.: Verified analysis of random binary tree structures. In: ITP 2018, volume 10895 of LNCS, pp. 196\u2013214 (2018)","DOI":"10.1007\/978-3-319-94821-8_12"},{"key":"9552_CR12","doi-asserted-by":"crossref","unstructured":"Erlingsson, U., Kaltofen, E., Musser, D.: Generic Gram\u2013Schmidt orthogonalization by exact division. In: ISSAC 1996, pp. 275\u2013282. ACM (1996)","DOI":"10.1145\/236869.237085"},{"key":"9552_CR13","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: Point-free, set-free concrete linear algebra. In: ITP\u00a02011, volume 6898 of LNCS, pp. 103\u2013118 (2011)","DOI":"10.1007\/978-3-642-22863-6_10"},{"key":"9552_CR14","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: FLOPS 2010, volume 6009 of LNCS, pp. 103\u2013117 (2010)","DOI":"10.1007\/978-3-642-12251-4_9"},{"issue":"2","key":"9552_CR15","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reason. 50(2), 173\u2013190 (2013)","journal-title":"J. Autom. Reason."},{"key":"9552_CR16","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-018-09504-w","volume":"64","author":"SJC Joosten","year":"2020","unstructured":"Joosten, S.J.C., Thiemann, R., Yamada, A.: A verified implementation of algebraic numbers in Isabelle\/HOL. J. Autom. Reason. 64, 363\u2013389 (2020)","journal-title":"J. Autom. Reason."},{"key":"9552_CR17","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BF01457454","volume":"261","author":"AK Lenstra","year":"1982","unstructured":"Lenstra, A.K., Lenstra, H.W., Lov\u00e1sz, L.: Factoring polynomials with rational coefficients. Math. Ann. 261, 515\u2013534 (1982)","journal-title":"Math. Ann."},{"key":"9552_CR18","doi-asserted-by":"crossref","unstructured":"Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: CPP\u00a02016, pp. 66\u201375. ACM (2016)","DOI":"10.1145\/2854065.2854074"},{"key":"9552_CR19","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.scico.2017.05.001","volume":"164","author":"JA McCarthy","year":"2018","unstructured":"McCarthy, J.A., Fetscher, B., New, M.S., Feltey, D., Findler, R.B.: A Coq library for internal verification of running-times. Sci. Comput. Program. 164, 49\u201365 (2018)","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"9552_CR20","doi-asserted-by":"publisher","first-page":"2008","DOI":"10.1137\/S0097539700373039","volume":"30","author":"D Micciancio","year":"2000","unstructured":"Micciancio, D.: The shortest vector in a lattice is hard to approximate to within some constant. SIAM J. Comput. 30(6), 2008\u20132035 (2000)","journal-title":"SIAM J. Comput."},{"volume-title":"The LLL Algorithm-Survey and Applications. Information Security and Cryptography","year":"2010","key":"9552_CR21","unstructured":"Nguyen, P.Q., Vall\u00e9e, B. (eds.): The LLL Algorithm-Survey and Applications. Information Security and Cryptography. Springer, Berlin (2010)"},{"key":"9552_CR22","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Verified root-balanced trees. In: APLAS\u00a02017, volume 10695 of LNCS, pp. 255\u2013272 (2017)","DOI":"10.1007\/978-3-319-71237-6_13"},{"key":"9552_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics. Springer, Berlin (2014)"},{"key":"9552_CR24","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9552_CR25","unstructured":"Storjohann, A.: Faster algorithms for integer lattice basis reduction. Technical Report 249, Department of Computer Science, ETH\u00a0Zurich (1996)"},{"key":"9552_CR26","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: TPHOLs\u201909, volume 5674 of LNCS, pp. 452\u2013468 (2009)","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"9552_CR27","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle\/HOL. In: CPP\u00a02016, pp. 88\u201399. ACM (2016)","DOI":"10.1145\/2854065.2854073"},{"key":"9552_CR28","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/S0022-314X(01)92763-5","volume":"95","author":"M van Hoeij","year":"2002","unstructured":"van Hoeij, M.: Factoring polynomials and the knapsack problem. J. Number Theory 95, 167\u2013189 (2002)","journal-title":"J. Number Theory"},{"key":"9552_CR29","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139856065","volume-title":"Modern Computer Algebra","author":"J von zur Gathen","year":"2013","unstructured":"von zur Gathen, J., Gerhard, J.: Modern Computer Algebra, 3rd edn. Cambridge University Press, Cambridge (2013)","edition":"3"},{"key":"9552_CR30","unstructured":"Wolfram Research, Inc.: Mathematica Version 11.3. Champaign, Illinois (2018)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09552-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09552-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09552-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,8]],"date-time":"2021-06-08T23:29:24Z","timestamp":1623194964000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09552-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6]]},"references-count":30,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["9552"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09552-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,6]]},"assertion":[{"value":"15 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 June 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}