Article :Browse 3155 Download 2929
Received:December 24, 2017 Revised:January 03, 2018
Received:December 24, 2017 Revised:January 03, 2018
Abstract:With the rapid development of quantum hardware, people tend to believe that special-purpose quantum computers with more than 100 qubits will be available in 5 to 10 years. It is conceivable that, once this becomes a reality, the development of quantum software will be crucial in harnessing the power of quantum computers. However, due to the distinguishable features of quantum mechanics, such as the no-cloning of quantum information and the nonlocal effect of entanglement, developing correct and efficient quantum programs and communication protocols is a challenging issue. Formal verification methods, particularly model checking techniques, have proven effective in classical software design and system modelling. Therefore, formal verification of quantum software has received more and more attention recently. This article reviews recent research findings in verification of both sequential quantum programs and quantum communication protocols, with the focus placed on the work of the two authors' research groups. Future directions and challenges in this area are also discussed.
keywords: quantum computing program verification model checking verification of communication protocol
Foundation items:Key Research Program of Frontier Sciences, CAS (QYZDJ-SSW-SYS003); CAS/SAFEA Int'l Partnership Program for Creative Research Teams
Reference text:
FENG Yuan,YING Ming-Sheng.Verification of Quantum Programs.Journal of Software,2018,29(4):1085-1093
FENG Yuan,YING Ming-Sheng.Verification of Quantum Programs.Journal of Software,2018,29(4):1085-1093