Primality Testing is Polynomial-time: A Mechanised Verification of the AKS Algorithm
We present a formalisation of the Agrawal-Kayal-Saxena (AKS) algorithm, a deterministic polynomial-time primality test. This algorithm was first announced by the AKS team in 2002, later improved in 2004. Our work is based on the improved version, with Parts 1 and 2 aim at a formal proof of the correctness of the algorithm, and Part 3 aims at a formal analysis of the complexity of the algorithm. The entire work is carried out in the HOL4 theorem prover. The correctness of the AKS algorithm...[Show more]
|Collections||Open Access Theses|
|thesis.pdf||Thesis Material||943.06 kB||Adobe PDF|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.