Hierarchical Verification of Quantum Circuits

  • Sidi Mohamed BeillahiEmail author
  • Mohamed Yousri Mahmoud
  • Sofiène Tahar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9690)


In this paper, we introduce the idea of hierarchical verification for quantum circuits, where we use a powerful language, higher-order logic, to reason about quantum circuits formally. We propose a formal modeling and verification approach that captures quantum models built hierarchically from primitive optical quantum gates. The analysis and verification of composed circuits is done seamlessly based on dedicated mathematical foundations formalized in the HOL Light theorem prover. In order to demonstrate the effectiveness of the proposed infrastructure, we present the formal analysis of the controlled-phase gate and Shor’s factoring quantum circuits.


  1. 1.
    Politi, A., Matthews, J.C.F., O’Brien, J.L.: Shor’s quantum factoring algorithm on a photonic chip. Science 325(5945), 1221 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Beillahi, S.M., Mahmoud, M.Y.: Hierarchical Verification of Quantum Circuits (2016).
  3. 3.
    Beillahi, S.M., Mahmoud, M.Y., Tahar, S.: Optical Quantum Gates Formalization in HOL Light. Technical report, ECE Department, Concordia University, Montreal, QC, Canada, February 2016Google Scholar
  4. 4.
    Viamontes, G.F., Rajagopalan, M., Markov, I.L., Hayes, J.P.: Gate level simulation of quantum circuits. In: ASP-DAC, pp. 295–301 (2003)Google Scholar
  5. 5.
    Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  6. 6.
    Knill, E., Laflamme, R., Milburn, G.J.: A scheme for efficient quantum computation with linear optics. Nature 409, 46–52 (2001)CrossRefzbMATHGoogle Scholar
  7. 7.
    Kok, P., Munro, W.J., Nemoto, K., Ralph, T.C., Dowling, J.P., Milburn, G.J.: Linear optical quantum computing with photonic qubits. Rev. Mod. Phys. 79, 135–174 (2007)CrossRefGoogle Scholar
  8. 8.
    Mahmoud, M.Y., Panangaden, P., Tahar, S.: On the formal verification of optical quantum gates in HOL. In: Núñez, M., Güdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 198–211. Springer, Heidelberg (2015)CrossRefGoogle Scholar
  9. 9.
    Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formalization of infinite dimension linear spaces with application to quantum theory. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 413–427. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  10. 10.
    Mandel, L., Wolf, E.: Optical Coherence and Quantum Optics. Cambridge University Press, Cambridge, UK (1995)CrossRefGoogle Scholar
  11. 11.
    Feynman, R.P.: Simulating physics with computers. Int. J. Theor. Phys. 21(6–7), 467–488 (1982)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Franke-Arnold, S., Gay, S.J., Puthoor, I.V.: Quantum process calculus for linear optical quantum computing. In: Dueck, G.W., Miller, D.M. (eds.) RC 2013. LNCS, vol. 7948, pp. 234–246. Springer, Heidelberg (2013)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Sidi Mohamed Beillahi
    • 1
    Email author
  • Mohamed Yousri Mahmoud
    • 1
  • Sofiène Tahar
    • 1
  1. 1.Department of Electrical and Computer EngineeringConcordia UniversityMontrealCanada

Personalised recommendations