Skip to main content
SpringerLink
Log in

Hierarchical Verification of Quantum Circuits

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9690))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  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)

    Article  MathSciNet  MATH  Google Scholar 

  2. Beillahi, S.M., Mahmoud, M.Y.: Hierarchical Verification of Quantum Circuits (2016). http://hvg.ece.concordia.ca/projects/optics/hvqc.html

    Google Scholar 

  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 2016

    Google Scholar 

  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. Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  6. Knill, E., Laflamme, R., Milburn, G.J.: A scheme for efficient quantum computation with linear optics. Nature 409, 46–52 (2001)

    Article  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  10. Mandel, L., Wolf, E.: Optical Coherence and Quantum Optics. Cambridge University Press, Cambridge, UK (1995)

    Book  Google Scholar 

  11. Feynman, R.P.: Simulating physics with computers. Int. J. Theor. Phys. 21(6–7), 467–488 (1982)

    Article  MathSciNet  Google Scholar 

  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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada

    Sidi Mohamed Beillahi, Mohamed Yousri Mahmoud & Sofiène Tahar

Authors
  1. Sidi Mohamed Beillahi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mohamed Yousri Mahmoud
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sofiène Tahar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sidi Mohamed Beillahi .

Editor information

Editors and Affiliations

  1. University of Minnesota, Minneapolis, Minnesota, USA

    Sanjai Rayadurgam

  2. NASA Ames Research Center , Moffett Field, California, USA

    Oksana Tkachuk

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Beillahi, S.M., Mahmoud, M.Y., Tahar, S. (2016). Hierarchical Verification of Quantum Circuits. In: Rayadurgam, S., Tkachuk, O. (eds) NASA Formal Methods. NFM 2016. Lecture Notes in Computer Science(), vol 9690. Springer, Cham. https://doi.org/10.1007/978-3-319-40648-0_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40648-0_26

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40647-3

  • Online ISBN: 978-3-319-40648-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation