[19]M.S Ying and Y Feng, Quantum loop programs, Acta Informatica 47(2010,221-250 [20] M.S. Ying, N K. Yu, Y. Feng and R Y Duan, Verification of quantum programs, Science of Computer Programming, 78(2013)1679 1700. [] S G. Ying, Y. Feng, N. K. Yu and M. S. Ying, Reachability analysis of quantum Markov chains, Proceedings of the 24th International Conf erence on Concurrency Theory(CONCUr), 2013, pp 334-348 [22] Y.J. Li and M.S. Ying, (Un)decidable problems about reachability of quantum systems, Proceedings of the 25th International Conference on Concurrency Theory(COnCur), 2014, pp. 482-496 L23J S Perdrix, Quantum entanglement analysis based on Abstract Interpretation, Proceedings of the 15th International Symposium on Static Analysis(SAS), 2008, pp 270-282 L 24 P. Jorrand and S. Perdrix, Abstract interpretation techniques for quantum computation, In: Semantic Techniques in Quantum Computation (I. Mackie and S. Gay, eds ) Cambridge University Press 2010, pp. 206 L 25 K. Honda, Analysis of quantum entanglement in quantum programs using stabiliser formalism, Electronic Proceedings in Theoretical Computer Science 195(QPL 2015), pp. 262-272 L 26O. Brunet and P. Jorrand, Dynamic quantum logic for quantum programs, International Journal of Quantum Information, 2(2004)45-54 27] A. Baltag and S Smets, LQP: the dynamic logic of quantum information, Mathematical Structures in Computer Science, 16(2006)491 525 [28]R Chadha, P Mateus and A Sernadas, Reasoning about imperative quantum programs, Electronic Notes in Theoretical Computer Science 158200619-39 [29J Y. Feng, R. Y. Duan, Z. F Ji and M.S. Ying, Proof rules for the correctness of quantum programs, Theoretical Computer Science 386(2007)151-166 [30] Y Kakutani, A logic for formal verification of quantum program Proceedings of the 13th Asian Computing Science Conference(ASIAN 2009),pp.79-93［19］M. S. Ying and Y. Feng, Quantum loop programs, Acta Informatica, 47(2010), 221-250. ［20］M. S. Ying, N. K. Yu, Y. Feng and R. Y. Duan, Verification of quantum programs, Science of Computer Programming, 78(2013)1679- 1700. ［21］S. G. Ying, Y. Feng, N. K. Yu and M. S. Ying, Reachability analysis of quantum Markov chains, Proceedings of the 24th International Conference on Concurrency Theory (CONCUR), 2013, pp. 334-348. ［22］Y. J. Li and M. S. Ying, (Un)decidable problems about reachability of quantum systems, Proceedings of the 25th International Conference on Concurrency Theory (CONCUR), 2014, pp. 482-496. ［23］S. Perdrix, Quantum entanglement analysis based on Abstract Interpretation, Proceedings of the 15th International Symposium on Static Analysis (SAS), 2008, pp. 270-282. ［24］P. Jorrand and S. Perdrix, Abstract interpretation techniques for quantum computation, In: Semantic Techniques in Quantum Computation （I. Mackie and S. Gay, eds.）, Cambridge University Press 2010, pp. 206- 234. ［25］K. Honda, Analysis of quantum entanglement in quantum programs using stabiliser formalism, Electronic Proceedings in Theoretical Computer Science 195 (QPL 2015), pp. 262-272. ［26］O. Brunet and P. Jorrand, Dynamic quantum logic for quantum programs, International Journal of Quantum Information, 2(2004)45-54. ［27］A. Baltag and S. Smets, LQP: the dynamic logic of quantum information, Mathematical Structures in Computer Science, 16(2006)491- 525. ［28］R. Chadha, P. Mateus and A. Sernadas, Reasoning about imperative quantum programs, Electronic Notes in Theoretical Computer Science, 158(2006)19-39. ［29］Y. Feng, R. Y. Duan, Z. F. Ji and M. S. Ying, Proof rules for the correctness of quantum programs, Theoretical Computer Science， 386(2007)151-166. ［30］Y. Kakutani, A logic for formal verification of quantum programs, Proceedings of the 13th Asian Computing Science Conference (ASIAN 2009), pp. 79-93