Skip to main content
Thesis defences

PhD Oral Exam - Muhammad Umair Siddique

Formal Analysis of Geometrical Optics using Theorem Proving


Date & time
Thursday, November 26, 2015
10 a.m. – 1 p.m.
Cost

This event is free

Organization

School of Graduate Studies

Contact

Sharon Carey
514-848-2424, ext. 3802

Wheel chair accessible

Yes

When studying for a doctoral degree (PhD), candidates submit a thesis that provides a critical review of the current state of knowledge of the thesis subject as well as the student’s own contributions to the subject. The distinguishing criterion of doctoral graduate research is a significant and original contribution to knowledge.

Once accepted, the candidate presents the thesis orally. This oral exam is open to the public.

Abstract

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 are 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 has 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´erot 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.


Back to top

© Concordia University