Abstract:
Asymptotic notations characterize the limiting behavior of a function. They are extensively
used in many branches of mathematics and computer science particularly in analytical
number theory, combinatorics and computational complexity while analyzing algorithms.
Traditionally, the mathematical analysis involving these notations has been done by paper and-pencil proof methods or simulation, which do not provide accurate results. Due to the
enormous usage of computational algorithms in safety-critical domains these days, accuracy
of asymptotic analysis has become extremely important. We propose to use Formal meth ods, which is a computer based mathematical analysis technique, to perform asymptotic
analysis of algorithms. In order to introduce formal verification in this domain, this thesis
provides the higher-order-logic formalizations of O, Θ, Ω, o and ω notations and the formal
verification of most of their classical properties of interest. The formalization is based on
the theory of sets, real and natural numbers and has been done using the HOL4 theorem
prover. To demonstrate the practical usefulness and effectiveness of this formalization,
we utilize it to formally analyze the computational complexities of the insertion sort and
uniqueness of array elements algorithms. Our formalization bears immense potential for
the formal analysis of cryptographic protocols in which the asymptotic notations are used
to estimate the size of the key so that it will be infeasible to break a system using given
number of steps.
