微信服务号

微信订阅号

2025-4-5- 11
Home > Archive>Volume 29, Issue 4, 2018 >1085-1093. DOI:10.13328/j.cnki.jos.005536
PDF HTML XML Export Cite reminder
Verification of Quantum Programs
Author:
Affiliation:

Fund Project:

Key Research Program of Frontier Sciences, CAS (QYZDJ-SSW-SYS003); CAS/SAFEA Int'l Partnership Program for Creative Research Teams

  • Article
    • | |
  • Metrics
    • |
  • Reference [59]
    • |
  • Related [20]
    • | | |
  • Comments
    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.

    Reference
    [1] Wecker D, Svore KM. LIQUi|>:A software design architecture and domain-specific language for quantum computing. arXiv.org, vol. quant-ph. p. arXiv:1402.4467, 19-Feb-2014.
    [2] Häner T, Steiger DS, Svore K, Troyer M. A software methodology for compiling quantum programs. arXiv.org, vol. cs.PL. p. arXiv:1604.01401, 06-Apr-2016.
    [3] The Q# Programming Language. 2017. https://docs.microsoft.com/en-us/quantum/quantum-qr-intro?view=qsharp-preview
    [4] Green AS, Lumsdaine PL, Ross NJ, Selinger P, Valiron B. Quipper-A scalable quantum programming language. In:Proc. of the PLDI. 2013. 333-342.
    [5] JavadiAbhari A, Patil S, Kudrow D, Heckey J, Lvov A, Chong FT, Martonosi M. ScaffCC:Scalable compilation and analysis of quantum programs. arXiv.org, vol. quant-ph. pp. arXiv:1507.01902-17, 08-Jul-2015.
    [6] Lapets A, Roetteler M. Abstract resource cost derivation for logical quantum circuit descriptions. In:Proc. of the 1st Annual Workshop on Functional Programming Concepts in Domain-Specific Languages-FPCDSL 2013. New York, 2013. 35-42.[doi:10. 1145/2505351.2505358]
    [7] Lapets A, da Silva MP, Thome M, Adler A, Beal J, Roetteler M. QuaFL:A typed DSL for quantum programming. In:Proc. of the 1st Annual Workshop on Functional Programming Concepts in Domain-Specific Languages-FPCDSL 2013. New York, 2013. 19-26.[doi:10.1145/2505351.2505357]
    [8] Ying MS, Feng Y. An algebraic language for distributed quantum computing. IEEE Trans. on Computers, 2009,58(6):728-743.[doi:10.1109/TC.2009.13]
    [9] Ying MS, Feng Y. A flowchart language for quantum programming. IEEE Trans. on Software Engineering, 2011,37(4):466-485.[doi:10.1109/TSE.2010.94]
    [10] Ying MS, Feng Y. Quantum loop programs. Acta Informatica, 2010,47(4):221-250.[doi:10.1007/s00236-010-0117-4]
    [11] Ying MS, Yu N, Feng Y, Duan R. Verification of quantum programs. Science of Computer Programming, 2013,78(9):1679-1700.[doi:10.1016/j.scico.2013.03.016]
    [12] Perdrix S. Quantum entanglement analysis based on abstract interpretation. In:Proc. of the SAS. 2008. 270-282.[doi:10.1007/978-3-540-69166-2_18]
    [13] Jorrand P, Perdrix S. Abstract interpretation techniques for quantum computation. In:Gay S, Mackie I, eds. Semantic Techniques in Quantum Computation. Cambridge:Cambridge University Press, 2009,(6):206-234.
    [14] Honda K. Analysis of quantum entanglement in quantum programs using stabilizer formalism. Electronic Proc. in Theoretical Computer Science, 2015,195(1):262-272.[doi:10.4204/EPTCS.195.19]
    [15] Brunet O, Jorrand P. Dynamic quantum logic for quantum programs. Int'l Journal of Quantum Information, 2011,2(1):45-54.[doi:10.1142/S0219749904000067]
    [16] Baltag A, Smets S. LQP:The dynamic logic of quantum information. Math. Struct. in Comp. Science, 2006,16(3):491-525.[doi:10. 1017/S0960129506005299]
    [17] Feng Y, Duan R, Ji Z, Ying MS. Proof rules for the correctness of quantum programs. Theoretical Computer Science, 2007,386(1):151-166.[doi:10.1016/j.tcs.2007.06.011]
    [18] Chadha R, Mateus P, Sernadas A. Reasoning about imperative quantum programs. Electronic Notes in Theoretical Computer Science, 2006.[doi:10.1016/j.entcs.2006.04.003]
    [19] Kakutani Y. A logic for formal verification of quantum programs. In:Proc. of the ASIAN. 2009.[doi:10.1007/978-3-642-10622-4_7]
    [20] Ying MS. Floyd-Hoare logic for quantum programs. Trans. on Programming Languages and Systems, 2011,33(6):1-49.[doi:10. 1145/2049706.2049708]
    [21] Liu T, Li Y, Wang S, Ying MS, Zhan N. A theorem prover for quantum hoare logic and its applications. arXiv.org, vol. cs.LO. p. arXiv:1601.03835, 15-Jan-2016.
    [22] Hasuo I, Hoshino N. Semantics of higher-order quantum computation via geometry of interaction. Annals of Pure and Applied Logic, 2017.[doi:10.1109/LICS.2011.26]
    [23] Pagani M, Selinger P, Valiron B. Applying quantitative semantics to higher-order quantum computing. In:Proc. of the POPL. 2014.[doi:10.1145/2578855.2535879]
    [24] Jacobs B. On block structures in quantum computation. Electronic Notes in Theoretical Computer Science, 2013,298:233-255.[doi:10.1016/j.entcs.2013.09.016]
    [25] Staton S. Algebraic effects, linearity, and quantum programming languages. In:Proc. of the 42nd Annual ACM SIGPLAN-SIGACT Symp. New York, 2015. 395-406.[doi:10.1145/2775051.2676999]
    [26] D'Hondt E, Panangaden P. Quantum weakest preconditions. Mathematical Structures in Computer Science, 2006.[doi:10.1017/S0960129506005251]
    [27] Ying MS, Duan R, Feng Y, Ji Z. Predicate transformer semantics of quantum programs. In:Gay S, Mackie I, eds. Semantic Techniques in Quantum Computation. Cambridge:Cambridge University Press, 2009,(8):311-360.
    [28] Ying S, Feng Y, Yu N, Ying MS. Reachability probabilities of quantum Markov chains. In:Proc. of the CONCUR. 2013. 334-348.[doi:10.1007/978-3-642-40184-8_24]
    [29] Yu N, Ying MS. Reachability and termination analysis of concurrent quantum programs. In:Proc. of the CONCUR. 2012. 69-83.[doi:10.1007/978-3-642-32940-1_7]
    [30] Li Y, Ying MS. (Un)deciddable problems about reachability of quantum systems. In:Proc. of the CONCUR. 2014. 482-496.[doi:10.1007/978-3-662-44584-6_33]
    [31] Feng Y, Yu N, Ying MS. Model checking quantum Markov chains. Journal of Computer and System Sciences, 2013,79(7):1181-1198.[doi:10.1016/j.jcss.2013.04.002]
    [32] Vardi YM. Automatic verification of probabilistic concurrent finite-state programs. In:Proc. of the FOCS. 1985.[doi:10.1109/SFCS.1985.12]
    [33] Diestel J, Uhl J. Vector Measures, vol. 15. Providence:American Mathematical Society, 1977.
    [34] Feng Y, Hahn EM, Turrini A, Zhang L. QPMC:A model checker for quantum programs and protocols. In:Proc. of the FM. 2015. 265-272.[doi:10.1007/978-3-319-19249-9_17]
    [35] Kwiatkowska MZ, Norman G, Parker D. PRISM 4.0-Verification of probabilistic real-time systems. In:Proc. of the CAV. 2011.[doi:10.1007/978-3-642-22110-1_47]
    [36] Anticoli L, Piazza C, Taglialegne L, Zuliani P. Towards quantum programs verification-From quipper circuits to QPMC. In:Proc. of the RC. 2016.[doi:10.1007/978-3-319-40578-0_16]
    [37] Feng Y, Hahn EM, Turrini A, Ying S. Model checking Omega-regular properties for quantum Markov chains. In:Proc. of the CONCUR. 2017. 35:1-35:16.[doi:10.1007/978-3-540-78499-9_22]
    [38] Feng Y, Yu N, Ying MS. Reachability analysis of recursive quantum Markov chains. In:Proc. of the MFCS. 2013. 385-396.[doi:10.1007/978-3-642-40313-2_35]
    [39] Etessami K, Yannakakis M. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. Journal of the ACM, 2009,1.[doi:10.1145/1462153.1462154]
    [40] Esparza J, Kiefer S, Luttenberger M. Newtonian program analysis. Journal of the ACM, 2010,57(6):1-47.[doi:10.1145/1857914. 1857917]
    [41] Advancing Quantum Information Science:National Challenges and Opportunities. 2016. https://www.whitehouse.gov/sites/whitehouse.gov/files/images/Quantum_Info_Sci_Report_2016_07_22%20final.pdf
    [42] Jorrand P, Lalire M. Toward a quantum process algebra. In:Proc. of the 1st Conf. on Computing Frontiers on Computing Frontiers. New York, 2004. 111-119.
    [43] Lalire M. Relations among quantum processes:bisimilarity and congruence. Mathematical Structures in Computer Science, 2006, 16(3):407.[doi:10.1017/S096012950600524X]
    [44] Gay S, Nagarajan R. Communicating quantum processes. In:Proc. of the POPL. 2005.[doi:10.1145/1040305.1040318]
    [45] Feng Y. Duan R. Ji Z, Ying M. Probabilistic bisimulations for quantum processes. Information and Computation, 2007,205(11):1608-1639.[doi:10.1016/j.ic.2007.08.001]
    [46] Ying MS, Feng Y, Duan R, Ji Z. An algebra of quantum processes. ACM Trans. on Computational Logic (TOCL), 2009,10(3):19-36.[doi:10.1145/1507244.1507249]
    [47] Feng Y, Duan R, Ying MS. Bisimulation for quantum processes. In:Proc. of the POPL. New York, 2011. 523-534.[doi:10.1145/1926385.1926446]
    [48] Feng Y, Duan R, Ying MS. Bisimulation for quantum processes. Trans. on Programming Languages and Systems, 2012,34(4):1-43.
    [49] Deng Y, Feng Y. Open bisimulation for quantum processes. In:Proc. of the IFIP TCS. 2012.[doi:10.1007/978-3-642-33475-7_9]
    [50] Feng Y, Deng Y, Ying MS. Symbolic bisimulation for quantum processes. ACM Trans. on Computational Logic, 2014,15(2):1-32.[doi:10.1145/2579818]
    [51] Hennessy M, Lin H. Symbolic bisimulations. Theoretical Computer Science, 1995,138(2):353-389.
    [52] Kubota T, Kakutani Y, Kato G, Kawano Y, Sakurada H. Semi-Automated verification of security proofs of quantum cryptographic protocols. Journal of Symbolic Computation, 2016,73:192-220.[doi:10.1016/j.jsc.2015.05.001]
    [53] Feng Y, Ying MS. Toward automatic verification of quantum cryptographic protocols. In:Proc. of the CONCUR. 2015. 441-455.
    [54] Deng Y, Feng Y, Lago UD. On coinduction and quantum Lambda Calculi. In:Proc. of the CONCUR. 2015. 427-440.
    [55] Ardeshir-Larijani E, Gay SJ, Nagarajan R. Equivalence checking of quantum protocols. In:Proc. of the TACAS. Berlin, Heidelberg, 2013,7795(33):478-492.[doi:10.1007/978-3-642-36742-7_33]
    [56] Ardeshir-Larijani E, Gay SJ, Nagarajan R. Verification of concurrent quantum protocols by equivalence checking. In:Proc. of the TACAS. Berlin, Heidelberg, 2014,8413(42):500-514.[doi:10.1007/978-3-642-54862-8_42]
    [57] Altenkirch T, Grattage J. A functional quantum programming language. In:Proc. of the LICS. 2005. 249-258.
    [58] Bădescu C, Panangaden P. Quantum alternation:Prospects and problems. Electronic Proc. in Theoretical Computer Science, 2015, 195(1):33-42.[doi:10.4204/EPTCS.195.3]
    [59] Ying MS. Foundations of Quantum Programming. Elsevier Science, 2016.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

冯元,应明生.量子程序验证.软件学报,2018,29(4):1085-1093

Copy
Share
Article Metrics
  • Abstract:4569
  • PDF: 8178
  • HTML: 4537
  • Cited by: 0
History
  • Received:December 24,2017
  • Revised:January 03,2018
  • Online: January 09,2018
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2033159Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063