Quantum computing systems promise to increase the efficiency of solving problems which classical computers cannot handle efficiently, such as integers factorization. In this paper, we introduce the idea of design automation for quantum circuits, where we build a rich library of quantum gates and develop a robust decision procedure in higher-order logic, to reason about quantum circuits formally. We adopt the low level optical modeling of quantum gates. Interestingly, this modeling provides optimized implementations for certain quantum gates that cannot be attained at the behavioral level. The constructed library contains a variety of quantum gates ranging from 1-qubit to 3-qubit gates that are sufficient to model most existing quantum circuits. To eliminate the user's interaction with the theorem prover, we develop a decision procedure that fully automates the analysis process. As real world applications, we present the formal analysis of several quantum circuits including the quantum full adder and the Grover's oracle circuits, for which we have proved the behavioral correctness and calculated the operational success rate which has never been provided in the literature. Furthermore, we show the efficiency of the proposed framework in terms of scalability and modularity.

HOL Script

• README
• HOL Light source
  
  

Publications

1. S.M. Beillahi, M.Y. Mahmoud and S. Tahar: Hierarchical Verification of Quantum Circuits [In: S. Rayadurgam and O. Tkachuk (Eds.), NASA Formal Methods Symposium (NFM'16), Lecture Notes in Computer Science 9690, Springer Verlag, 2016, pp. 1-9.]
   
   
2. S.M. Beillahi, M.Y. Mahmoud and S. Tahar: Optical Quantum Gates Formalization in HOL Light [Technical Report, Department of Electrical and Computer Engineering, Concordia University, February 2016, pp. 1-35]
   
   
3. S.M. Beillahi, M.Y. Mahmoud and S. Tahar: A Tool for the Formal Verification of Quantum Optical Computing Systems [Proc. Automated Reasoning Workshop (ARW'15), Birmingham, United Kingdom, April, 2015, pp. 25-26.]
   
   
4. S.M. Beillahi, M.Y. Mahmoud and S. Tahar: Modeling and Verification of Quantum Optics Circuits [A poster in: IEEE-OSA Montreal Poster Competition, 2016]