Geometrical optics, in which light is characterized as rays or beams, provides an efficient and scalable formalism for the modeling and analysis of optical and laser systems. The main applications of geometrical optics are in stability analysis of optical resonators, laser mode locking and Quasi-optical systems. Traditionally, the analysis of such applications has been carried out by informal techniques like paper-and-pencil proof methods, simulation and computer algebra systems. In this research project, we propose a higher-order logic formalization of geometrical optics which includes optical imaging, optical resonators and Gaussian beams. Our formalization is mainly based on theories of multivariate analysis in the HOL Light theorem prover. 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-Perot resonator, an optical phase-conjugated ring resonator and a receiver module of the APEX telescope.

HOL Script

• README
• HOL Light source
  
  

Publications

1. U. Siddique and S. Tahar: Formal Verification of Stability and Chaos in Periodic Optical Systems, Journal of Computer and System Sciences, Elsevier, Vol. 88, September 2017, pp. 271-289.
   
   
2. U. Siddique and S. Tahar: On the Formal Analysis of Gaussian Optical Systems in HOL, Formal Aspects of Computing, Springer, Vol. 28, No. 5, September 2016, pp 881-907.
   
   
3. U. Siddique and S. Tahar: On the Formalization of Cardinal Points of Optical Systems [In: T. Bouabana-Tebibel and H. S. Rubin (Eds.), Formalisms for Reuse and Systems Integration, Advances in Intelligent Systems and Computing, Volume 346, Springer 2015, pp. 79-102]
   
   
4. C. Kaliszyk, J. Urban, U. Siddique, S. Khan-Afshar, C. Dunchev and S. Tahar: Formalizing Physics: Automation, Presentation and Foundation Issues [In: M. Kerber, J. Carette, C. Kaliszyk, F. Rabe and V. Sorge (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science Volume 9150, pp 288-295]
   
   
5. U. Siddique and S. Tahar: Stability Verification of Optical and Laser Resonators in HOL Light [Technical Report, Department of Electrical and Computer Engineering, Concordia University, November 2014, pp. 1-12]
   
   
6. U. Siddique and S. Tahar: Towards Ray Optics Formalization of Optical Imaging Systems [Proceedings of IEEE International Conference on Information Reuse and Integration (IRI'14), San Francisco, California, USA, 2014, pp. 378-385.]
   
   
7. U. Siddique and S. Tahar: A Framework for Formal Reasoning about Geometrical Optics [In: S. Watt, J. Davenport, A. Sexton, P. Sojka and J. Urban (Eds.), Intelligent Computer Mathematics (CICM'14), Lecture Notes in Computer Science 8543, Springer, pp. 453-456]
   
   
8. S. K. Afshar, U. Siddique, M. Y. Mahmoud, V. Aravantinos, O. Seddiki, O. Hasan, and S. Tahar: Formal Analysis of Optical Systems, Mathematics in Computer Science, Vol. 8, No. 1, Springer, May 2014, pp. 39-70.
   
   
9. U. Siddique and S. Tahar: Towards the Formal Analysis of Microresonators Based Photonic Systems [In: IEEE/ACM Design Automation and Test in Europe (DATE'14), Dresden, Germany, March 2014, pp. 1-6]
   
   
10. U. Siddique, V. Aravantinos, and S. Tahar: A New Approach for the Verification of Optical Systems [In: J. Sasin and R.N. Youngworth (Eds.), Optical System Alignment, Tolerancing, and Verification VII (SPIE'13), Proc. SPIE 8844, 2013, pp. 88440G1-88440G-14]
    
    
11. U. Siddique, V. Aravantinos, and S. Tahar: On the Formal Analysis of Geometrical Optics in HOL [In: T. Ida and J. Fleuriot (Eds.), Automated Deduction in Geometry, Lecture Notes in Computer Science 7993, Springer Verlag, 2013, pp. 161-180.]
    
    
12. U. Siddique, V. Aravantinos, and S. Tahar: Formal Stability Analysis of Optical Resonators [In: G. Brat, N. Rungta, and A. Venet (Eds.), NASA Formal Methods Symposium (NFM'13), Lecture Notes in Computer Science 7871, Springer Verlag, 2013, pp. 368-382.]
    
    
13. U. Siddique, V. Aravantinos and S. Tahar: Higher-Order Logic Formalization of Geometrical Optics [In: T. Ida and J. Fleuriot (Eds.), Automated Deduction in Geometry (ADG'12), Informatics Research Report, School of Informatics, University of Edinburgh, Edinburgh, UK, September 2012, pp. 184-196.]
    
    

PhD Thesis

Muhammad Umair Siddique, "Formal Analysis of Geometrical Optics using Theorem Proving", PhD Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, December 2015.