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

## Publications

- 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]

- 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]

- 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]

- 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]

- 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.

- 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.]

- 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.]