### 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 language | English |
---|---|

Title of host publication | CPP 2017 |

Subtitle of host publication | Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs |

Publisher | Association for Computing Machinery (ACM) |

Pages | 17-29 |

Number of pages | 13 |

ISBN (Print) | 978-1-4503-4705-1 |

DOIs | |

Publication status | Published - 2017 |

Event | 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017 - Paris, France Duration: 16 Jan 2017 → 17 Jan 2017 Conference number: 6 |

### Conference

Conference | 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017 |
---|---|

Country | France |

City | Paris |

Period | 16/01/17 → 17/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