Skip to main content


Weitere Artikel dieser Ausgabe durch Wischen aufrufen

17.06.2019 | Ausgabe 4/2020 Open Access

Journal of Automated Reasoning 4/2020

A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm

Journal of Automated Reasoning > Ausgabe 4/2020
Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada
Wichtige Hinweise
This research was supported by the Austrian Science Fund (FWF) Project Y757. Jose Divasón is partially funded by the Spanish Projects MTM2014-54151-P and MTM2017-88804-P. Sebastiaan is now working at University of Twente, The Netherlands, and supported by the NWO VICI 639.023.710 Mercedes project. Akihisa is now working at National Institute of Informatics, Japan, and supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST. The authors are listed in alphabetical order regardless of individual contributions or seniority.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.


We formally verify the Berlekamp–Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun’s square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs factorization in the prime field \(\mathrm {GF}(p){}\) and then performs computations in the ring of integers modulo \(p^k\), where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using locales and local type definitions. Through experiments we verify that our algorithm factors polynomials of degree up to 500 within seconds.

Unsere Produktempfehlungen

Premium-Abo der Gesellschaft für Informatik

Sie erhalten uneingeschränkten Vollzugriff auf alle acht Fachgebiete von Springer Professional und damit auf über 45.000 Fachbücher und ca. 300 Fachzeitschriften.

Über diesen Artikel

Weitere Artikel der Ausgabe 4/2020

Journal of Automated Reasoning 4/2020 Zur Ausgabe

Premium Partner