{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T18:55:04Z","timestamp":1784314504138,"version":"3.55.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2019,6,17]],"date-time":"2019-06-17T00:00:00Z","timestamp":1560729600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,6,17]],"date-time":"2019-06-17T00:00:00Z","timestamp":1560729600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Austrian Science Fund","award":["Y757"],"award-info":[{"award-number":["Y757"]}]},{"name":"Austrian Science Fund","award":["Y757"],"award-info":[{"award-number":["Y757"]}]},{"name":"Austrian Science Fund","award":["Y757"],"award-info":[{"award-number":["Y757"]}]},{"DOI":"10.13039\/501100003329","name":"Ministerio de Econom\u00eda y Competitividad","doi-asserted-by":"crossref","award":["MTM2014-54151-P"],"award-info":[{"award-number":["MTM2014-54151-P"]}],"id":[{"id":"10.13039\/501100003329","id-type":"DOI","asserted-by":"crossref"}]},{"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":"publisher","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}],"id":[{"id":"10.13039\/501100002241","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,4]]},"DOI":"10.1007\/s10817-019-09526-y","type":"journal-article","created":{"date-parts":[[2019,6,17]],"date-time":"2019-06-17T14:03:06Z","timestamp":1560780186000},"page":"699-735","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Verified Implementation of the Berlekamp\u2013Zassenhaus Factorization Algorithm"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5173-128X","authenticated-orcid":false,"given":"Jose","family":"Divas\u00f3n","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6590-6220","authenticated-orcid":false,"given":"Sebastiaan J. C.","family":"Joosten","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0323-8829","authenticated-orcid":false,"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8872-2240","authenticated-orcid":false,"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,6,17]]},"reference":[{"key":"9526_CR1","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1016\/j.jsc.2012.09.004","volume":"50","author":"J Abbott","year":"2013","unstructured":"Abbott, J.: Bounds on factors in $$Z[x]$$. J. Symb. Comput. 50, 532\u2013563 (2013)","journal-title":"J. Symb. Comput."},{"key":"9526_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/b97662","volume-title":"Linear Algebra Done Right. Undergraduate Texts in Mathematics","author":"SJ Axler","year":"1997","unstructured":"Axler, S.J.: Linear Algebra Done Right. Undergraduate Texts in Mathematics. Springer, Berlin (1997)"},{"issue":"2","key":"9526_CR3","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":"9526_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., Olmedo, F., B\u00e9guelin, S.Z.: Verified indifferentiable hashing into elliptic curves. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. POST\u00a02012, Volume 7215 of LNCS, pp. 209\u2013228. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28641-4_12"},{"issue":"8","key":"9526_CR5","doi-asserted-by":"publisher","first-page":"1853","DOI":"10.1002\/j.1538-7305.1967.tb03174.x","volume":"46","author":"ER Berlekamp","year":"1967","unstructured":"Berlekamp, E.R.: Factoring polynomials over finite fields. Bell Syst. Tech. J. 46(8), 1853\u20131859 (1967)","journal-title":"Bell Syst. Tech. J."},{"key":"9526_CR6","unstructured":"Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for higher-order logic. In: ACM\/IEEE Symposium on Logic in Computer Science, LICS 32, pp. 1\u201312. IEEE Computer Society (2017). Cross-type induction is explained in Appendix\u00a0D of the extended report version at \nhttp:\/\/matryoshka.gforge.inria.fr\/pubs\/nonuniform_report.pdf"},{"key":"9526_CR7","unstructured":"Bottesch, R., Haslbeck, M.W., Thiemann, R.: A verified efficient implementation of the LLL basis reduction algorithm. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) Logic for Programming, Artificial Intelligence and Reasoning. LPAR\u00a022, Volume\u00a057 of EPiC Series in Computing, pp. 164\u2013180. EasyChair (2018)"},{"issue":"154","key":"9526_CR8","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1090\/S0025-5718-1981-0606517-5","volume":"36","author":"DG Cantor","year":"1981","unstructured":"Cantor, D.G., Zassenhaus, H.: A new algorithm for factoring polynomials over finite fields. Math. Comput. 36(154), 587\u2013592 (1981)","journal-title":"Math. Comput."},{"issue":"1","key":"9526_CR9","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0747-7171(87)80050-0","volume":"4","author":"L Cerlienco","year":"1987","unstructured":"Cerlienco, L., Mignotte, M., Piras, F.: Computing the measure of a polynomial. J. Symb. Comput. 4(1), 21\u201333 (1987)","journal-title":"J. Symb. Comput."},{"key":"9526_CR10","doi-asserted-by":"crossref","unstructured":"Divas\u00f3n, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A formalization of the Berlekamp\u2013Zassenhaus factorization algorithm. In: Bertot, Y., Vafeiadis, V. (eds.) Certified Programs and Proofs. CPP 2017, pp. 17\u201329. ACM (2017)","DOI":"10.1145\/3018610.3018617"},{"key":"9526_CR11","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: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving. ITP 2018, Volume 10895 of LNCS, pp. 160\u2013177. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-94821-8_10"},{"key":"9526_CR12","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming. FLOPS\u00a02010, Volume 6009 of LNCS, pp. 103\u2013117. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-12251-4_9"},{"issue":"2","key":"9526_CR13","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."},{"issue":"2","key":"9526_CR14","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(2), 167\u2013189 (2002)","journal-title":"J. Number Theory"},{"key":"9526_CR15","doi-asserted-by":"crossref","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Certified Programs and Proofs. CPP\u00a02013, Volume 8307 of LNCS, pp. 131\u2013146. Springer, Berlin (2013)","DOI":"10.1007\/978-3-319-03545-1_9"},{"issue":"7","key":"9526_CR16","first-page":"595","volume":"7","author":"A Karatsuba","year":"1963","unstructured":"Karatsuba, A., Ofman, Y.: Multiplication of multidigit numbers on automata. Sov. Phys. Dokl. 7(7), 595\u2013596 (1963)","journal-title":"Sov. Phys. Dokl."},{"key":"9526_CR17","unstructured":"Kirkels, B.: Irreducibility certificates for polynomials with integer coefficients. Master\u2019s thesis, Radboud Universiteit Nijmegen (2004)"},{"key":"9526_CR18","volume-title":"The Art of Computer Programming, Volume 2: Seminumerical Algorithms","author":"DE Knuth","year":"1998","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 2: Seminumerical Algorithms, 3rd edn. Addison-Wesley, Reading (1998)","edition":"3"},{"key":"9526_CR19","unstructured":"Kobayashi, H., Suzuki, H., Ono, Y.: Formalization of Hensel\u2019s lemma. In: Hurd, J., Smith, E., Darbari, A. (eds.) Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, pp. 114\u2013118. Oxford University Computing Laboratory (2005)"},{"key":"9526_CR20","doi-asserted-by":"crossref","unstructured":"Krauss, A.: Recursive definitions of monadic functions. In: Bove, A., Komendantskaya, E., Niqui, M. (eds.) Partiality and Recursion in Interactive Theorem Provers. PAR\u00a02010, Volume\u00a043 of EPTCS, pp. 1\u201313 (2010)","DOI":"10.4204\/EPTCS.43.0"},{"issue":"2","key":"9526_CR21","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s10817-018-9464-6","volume":"62","author":"O Kun\u010dar","year":"2019","unstructured":"Kun\u010dar, O., Popescu, A.: From types to sets by local type definition in higher-order logic. J. Autom. Reason. 62(2), 237\u2013260 (2019)","journal-title":"J. Autom. Reason."},{"key":"9526_CR22","unstructured":"Lee, H.: Vector spaces. Archive of Formal Proofs, Formal proof development. \nhttp:\/\/isa-afp.org\/entries\/VectorSpace.html\n\n (2014)"},{"key":"9526_CR23","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":"9526_CR24","doi-asserted-by":"crossref","unstructured":"Lochbihler, A.: Fast machine words in Isabelle\/HOL. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving. ITP\u00a02018, Volume 10895 of LNCS, pp. 388\u2013410. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-94821-8_23"},{"key":"9526_CR25","unstructured":"Maple 2017.3. Maplesoft, a division of Waterloo Maple Inc. Waterloo (2017)"},{"issue":"1","key":"9526_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-014-9312-2","volume":"54","author":"\u00c9 Martin-Dorel","year":"2015","unstructured":"Martin-Dorel, \u00c9., Hanrot, G., Mayero, M., Th\u00e9ry, L.: Formally verified certificate checkers for hardest-to-round computation. J. Autom. Reason. 54(1), 1\u201329 (2015)","journal-title":"J. Autom. Reason."},{"issue":"128","key":"9526_CR27","doi-asserted-by":"publisher","first-page":"1153","DOI":"10.1090\/S0025-5718-1974-0354624-3","volume":"28","author":"M Mignotte","year":"1974","unstructured":"Mignotte, M.: An inequality about factors of polynomials. Math. Comput. 28(128), 1153\u20131157 (1974)","journal-title":"Math. Comput."},{"issue":"3","key":"9526_CR28","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/1086837.1086844","volume":"8","author":"A Miola","year":"1974","unstructured":"Miola, A., Yun, D.Y.: Computational aspects of Hensel-type univariate polynomial greatest common divisor algorithms. ACM SIGSAM Bull. 8(3), 46\u201354 (1974)","journal-title":"ACM SIGSAM Bull."},{"key":"9526_CR29","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, Volume 2283 of LNCS","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, Volume 2283 of LNCS. Springer, Berlin (2002)"},{"key":"9526_CR30","unstructured":"Thiemann, R.: Computing n-th roots using the Babylonian method. Archive of Formal Proofs, Formal proof development. \nhttp:\/\/isa-afp.org\/entries\/Sqrt_Babylonian.html\n\n (2013)"},{"key":"9526_CR31","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Yamada, A.: Algebraic numbers in Isabelle\/HOL. In: Blanchette, J., Merz, S. (eds.) Interactive Theorem Proving. ITP\u00a02016, Volume 9807 of LNCS, pp. 391\u2013408. Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-43144-4_24"},{"key":"9526_CR32","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle\/HOL. In: Avigad, J., Chlipala, A. (eds.) Certified Programs and Proofs. CPP\u00a02016, pp. 88\u201399. ACM (2016)","DOI":"10.1145\/2854065.2854073"},{"key":"9526_CR33","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139856065","volume-title":"Modern Computer Algebra","author":"J von\u00a0zur Gathen","year":"2013","unstructured":"von\u00a0zur Gathen, J., Gerhard, J.: Modern Computer Algebra, 3rd edn. Cambridge University Press, Cambridge (2013)","edition":"3"},{"key":"9526_CR34","unstructured":"Mathematica Version 11.2. Wolfram Research, Inc. Champaign (2017)"},{"key":"9526_CR35","doi-asserted-by":"crossref","unstructured":"Yun, D.Y.: On square-free decomposition algorithms. In: Symbolic and Algebraic Computation. SYMSAC\u00a01976, pp. 26\u201335. ACM (1976)","DOI":"10.1145\/800205.806320"},{"issue":"3","key":"9526_CR36","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0022-314X(69)90047-X","volume":"1","author":"H Zassenhaus","year":"1969","unstructured":"Zassenhaus, H.: On Hensel factorization, I. J. Number Theory 1(3), 291\u2013311 (1969)","journal-title":"J. Number Theory"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09526-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-019-09526-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09526-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,15]],"date-time":"2020-06-15T23:08:35Z","timestamp":1592262515000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-019-09526-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,17]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["9526"],"URL":"https:\/\/doi.org\/10.1007\/s10817-019-09526-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,6,17]]},"assertion":[{"value":"17 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 May 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 June 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}