A formalization of the Berlekamp-Zassenhaus factorization algorithm

Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    9 Citations (Scopus)

    Abstract

    We formalize 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 a factorization in the prime field GF(p) and then performs computations in the ring of integers modulo pk, 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 Isabelle’s recent addition of local type definitions. Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds.
    Original languageEnglish
    Title of host publicationCPP 2017
    Subtitle of host publicationProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
    PublisherAssociation for Computing Machinery (ACM)
    Pages17-29
    Number of pages13
    ISBN (Print)978-1-4503-4705-1
    DOIs
    Publication statusPublished - 2017
    Event6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017 - Paris, France
    Duration: 16 Jan 201717 Jan 2017
    Conference number: 6

    Conference

    Conference6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017
    CountryFrance
    CityParis
    Period16/01/1717/01/17

    Fingerprint Dive into the research topics of 'A formalization of the Berlekamp-Zassenhaus factorization algorithm'. Together they form a unique fingerprint.

  • Cite this

    Divasón, J., Joosten, S., Thiemann, R., & Yamada, A. (2017). A formalization of the Berlekamp-Zassenhaus factorization algorithm. In CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (pp. 17-29). Association for Computing Machinery (ACM). https://doi.org/10.1145/3018610.3018617