Mr. Umair Siddique Profile

Umair Siddique

SPIE Involvement:

Author

Publications (1)

This will count as one of your downloads.

You will have access to both the presentation and article (if available).

DOWNLOAD NOW

This content is available for download via your institution's subscription. To access this item, please sign in to your personal account.

Email or Username Forgot your username?

Password Forgot your password?

Show

Keep me signed in

No SPIE account? Create an account

Proceedings Article | 10 September 2013 Paper

A new approach for the verification of optical systems

Umair Siddique, Vincent Aravantinos, Sofiène Tahar

Proceedings Volume 8844, 88440G (2013) https://doi.org/10.1117/12.2024860

KEYWORDS: Resonators, Interfaces, Free space, Optical components, Spherical lenses, Computing systems, Logic, Geometrical optics, Systems modeling, Optical resonators

Read Abstract +

Optical systems are increasingly used in microsystems, telecommunication, aerospace and laser industry. Due to the complexity and sensitivity of optical systems, their verification poses many challenges to engineers. Traditionally, the analysis of such systems has been carried out by paper-and-pencil based proofs and numerical computations. However, these techniques cannot provide perfectly accurate results due to the risk of human error and inherent approximations of numerical algorithms. In order to overcome these limitations, we propose to use theorem proving (i.e., a computer-based technique that allows to express mathematical expressions and reason about them by taking into account all the details of mathematical reasoning) as an alternative to computational and numerical approaches to improve optical system analysis in a comprehensive framework. In particular, this paper provides a higher-order logic (a language used to express mathematical theories) formalization of ray optics in the HOL Light theorem prover. Based on the multivariate analysis library of HOL Light, we formalize the notion of light ray and optical system (by defining medium interfaces, mirrors, lenses, etc.), i.e., we express these notions mathematically in the software. This allows us to derive general theorems about the behavior of light in such optical systems. In order to demonstrate the practical effectiveness, we present the stability analysis of a Fabry-Perot resonator.

My Library

You currently do not have any folders to save your paper to! Create a new folder below.

Folder Name

Folder Description

View contact details

UPDATE YOUR PROFILE

Is this your profile? Update it now.

Sign into your SPIE.org account

Don’t have a profile and want one?

Create an account on SPIE.org

Access to the requested content is limited to institutions that have purchased or subscribe to SPIE eBooks. You are receiving this notice because your organization may not have SPIE eBooks access.*

*Shibboleth/Open Athens users─please sign in to access your institution's subscriptions.

To obtain this item, you may purchase the complete book in print or electronic format on SPIE.org.

ORGANIZATIONAL
Sign in with credentials provided by your organization.

Organizational Username

Organizational Password

Show/Hide Password

INSTITUTIONAL
Select your institution to access the SPIE Digital Library.

SELECT YOUR INSTITUTION

PERSONAL
Sign in with your SPIE account to access your personal subscriptions or to use specific features such as save to my library, sign up for alerts, save searches, etc.

PERSONAL SIGN IN

No SPIE Account? Create one

PURCHASE THIS CONTENT

SUBSCRIBE TO DIGITAL LIBRARY

50 downloads per 1-year subscription

Members: $195

Non-members: $335 ADD TO CART

25 downloads per 1 - year subscription

Members: $145

Non-members: $250 ADD TO CART

PURCHASE SINGLE ARTICLE

Includes PDF, HTML & Video, when available

Members:

Non-members: ADD TO CART

Keywords/Phrases

Search In:

Publication Years