### Abstract

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 |

Pages | 17-29 |

Number of pages | 13 |

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

DOIs | |

State | 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

### Cite this

*CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs*(pp. 17-29). Association for Computing Machinery. DOI: 10.1145/3018610.3018617

}

*CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs.*Association for Computing Machinery, pp. 17-29, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, 16/01/17. DOI: 10.1145/3018610.3018617

**A formalization of the Berlekamp-Zassenhaus factorization algorithm.** / Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A formalization of the Berlekamp-Zassenhaus factorization algorithm

AU - Divasón,Jose

AU - Joosten,Sebastiaan

AU - Thiemann,René

AU - Yamada,Akihisa

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

U2 - 10.1145/3018610.3018617

DO - 10.1145/3018610.3018617

M3 - Conference contribution

SN - 978-1-4503-4705-1

SP - 17

EP - 29

BT - CPP 2017

PB - Association for Computing Machinery

ER -