Skip navigation
Skip navigation
Open Research is currently experiencing some technical issues and is undergoing maintenance. Due to the technical issues some pages are displaying 'Internal System Error' pages rather than the expected page.

Primality Testing is Polynomial-time: A Mechanised Verification of the AKS Algorithm

Chan, Hing Lun Joseph


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]

CollectionsOpen Access Theses
Date published: 2019
Type: Thesis (PhD)
DOI: 10.25911/5f58b06ca124e


File Description SizeFormat Image
thesis.pdfThesis Material943.06 kBAdobe PDFThumbnail

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator