The theory of quantum optics led to a revolution in physics as it allows the development of numerous powerful, cutting edge engineering applications. The analysis and verification of such applications and systems, however, are very complicated. Moreover, traditional analysis tools, e.g., simulation are not well suited for quantum systems. In this project, we develop a verification framework for quantum optics and related applications based on higher-order logic theorem proving techniques. The framework consists of three major libraries: 1) Mathematical foundations, 2) Quantum mechanics preliminaries, and 3) Quantum Optics. On top of these theoretical foundations, we have built formal models of a number of optical devices commonly used in quantum circuits, such as beam splitters and light phase shifters. We have also formally verified a number of quantum optical computing circuits, including, the Flip gate, CNOT gate, and Mach-Zehnder interferometer.

HOL Scripts

• README
• HOL Light source
  
  

Publications

1. M.Y. Mahmoud, P. Panangaden and S. Tahar: On the Formal Verification of Optical Quantum Gates in HOL In: M. Nunes and M. Gudemann (Eds.), Formal Methods for Industrial Critical Systems, Lecture Notes in Computer Science 9128, 2015, pp. 198-211. [Proc. Formal Methods for Industrial Critical Systems (FMICS'15), Oslo, Norway, June, 2015]
   
   
2. S.M. Beillahi, M.Y. Mahmoud and S. Tahar: A Tool for the Formal Verification of Quantum Optical Computing Systems [Proceeding of Automated Reasoning Workshop (ARW'15), Birmingham, United Kingdom, April, 2015, pp. 25-26]
   
   
3. M.Y. Mahmoud, V. Aravantinos and S. Tahar: Formal Verification of Optical Quantum Flip Gate[In: G. Klein and R. Gamboa (Eds.), Interactive Theorem Proving (ITP'14), Lecture Notes in Computer Science 8558, Springer Verlag, 2014, pp. 358-373]
   
   
4. M. Y. Mahmoud, and S. Tahar: On the Quantum Formalization of Coherent Light in HOL [In: J. M. Badger, K. Y. Rozier (Eds.), NASA Formal Methods Symposium (NFM'14), Lecture Notes in Computer Science 8430 , Springer Verlag, 2014, pp. 128-142]
   
   
5. 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.
   
   
6. M.Y. Mahmoud, V. Aravantinos, and S. Tahar: Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory [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. 413-427.]
   
   
7. M.Y. Mahmoud, V. Aravantinos and S. Tahar: Towards the Formal Verification of Quantum Optical Systems [Proc. International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS.12), Kyoto, Japan, November 2012, pp. 147-151.]