Hierarchical Verification of Quantum Circuits
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.
- 2.Beillahi, S.M., Mahmoud, M.Y.: Hierarchical Verification of Quantum Circuits (2016). http://hvg.ece.concordia.ca/projects/optics/hvqc.html
- 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.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