Bertram Felgenhauer, Aart Middeldorp, Fabian Mitterwallner, and Julian Nagele
Proceedings of the 7th International Workshop on Confluence (IWC 2018), pp. 76, 2018.
pdf
Abstract
The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It thereby approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has several applications in number theory, computer algebra and cryptography.
In this paper, we develop the first mechanized soundness proof of the LLL algorithm using Isabelle/HOL. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.
BibTex
@inproceedings{BFAMFMJN-IWC18, author = "Bertram Felgenhauer and Aart Middeldorp and Fabian Mitterwallner and Julian Nagele", title = "{CoCo} 2018 Participant: {CSI} 1.2.1", booktitle = "Proceedings of the 7th International Workshop on Confluence", editor = "Bertram Felgenhauer and Jakob Grue Simonsen", pages = 76, year = 2018}