Login | Register

Formal Analysis of Geometrical Optics using Theorem Proving


Formal Analysis of Geometrical Optics using Theorem Proving

Siddique, Muhammad Umair (2015) Formal Analysis of Geometrical Optics using Theorem Proving. PhD thesis, Concordia University.

[thumbnail of SIDDIQUE_PhD_S2016.pdf]
Text (application/pdf)
SIDDIQUE_PhD_S2016.pdf - Accepted Version


Geometrical optics is a classical theory of Physics which describes the light propagation in the form of rays and beams.
One of its main advantages is efficient and scalable formalism for the modeling and analysis of a variety of optical
systems which are used in ubiquitous applications including telecommunication, medicine and biomedical devices.
Traditionally, the modeling and analysis of optical systems have been carried out by paper-and-pencil based proofs and
numerical algorithms. However, these techniques cannot provide perfectly accurate results due to the risk of human
error and inherent incompleteness of numerical algorithms. In this thesis, we propose a higher-order logic theorem
proving based framework to analyze optical systems. The main advantages of this framework are the expressiveness
of higher-order logic and the soundness of theorem proving systems which provide unrivaled analysis accuracy.
In particular, this thesis provides the higher-order logic formalization of geometrical optics including the notion of
light rays, beams and optical systems. This allows us to develop a comprehensive analysis support for optical resonators,
optical imaging and Quasi-optical systems. This thesis also facilitates the verification of some of the most interesting
optical system properties like stability, chaotic map generation, beam transformation and mode analysis. We use this
infrastructure to build a library of commonly used optical components such as lenses, mirrors and optical cavities.
In order to demonstrate the effectiveness of our proposed approach, we conduct the formal analysis of some
real-world optical systems, e.g., an ophthalmic device for eye, a Fabry-P\'{e}rot resonator, an optical
phase-conjugated ring resonator and a receiver module of the APEX telescope. All the above mentioned work is
carried out in the HOL Light theorem prover.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Siddique, Muhammad Umair
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Date:26 October 2015
Thesis Supervisor(s):Tahar, Sofiene
ID Code:980766
Deposited On:16 Jun 2016 15:48
Last Modified:18 Jan 2018 17:51
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top