{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T12:50:52Z","timestamp":1775739052579,"version":"3.50.1"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,2,12]],"date-time":"2019-02-12T00:00:00Z","timestamp":1549929600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,2,12]],"date-time":"2019-02-12T00:00:00Z","timestamp":1549929600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP160101652"],"award-info":[{"award-number":["DP160101652"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2019,2,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.<\/jats:p>","DOI":"10.1007\/s00165-018-0465-3","type":"journal-article","created":{"date-parts":[[2018,8,7]],"date-time":"2018-08-07T05:41:35Z","timestamp":1533620495000},"page":"3-25","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Toward automatic verification of quantum programs"],"prefix":"10.1145","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4847-702X","authenticated-orcid":false,"given":"Mingsheng","family":"Ying","sequence":"first","affiliation":[{"name":"Centre for Quantum Software and Information, University of Technology Sydney, 2007, Sydney, NSW, Australia"},{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"},{"name":"Department of Computer Science and Technology, Tsinghua University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Altenkirch T Grattage J (2005) A functional quantum programming language. In: Proceedings of the 20th IEEE symposium on logic in computer science (LICS) pp 249\u2013258","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Ambainis A Bach E Nayak A Vishwanath A Watrous J (2001) One-dimensional quantum walks. In: Proceedings of the 33rd ACM symposium on theory of computing (STOC) pp 37\u201349","DOI":"10.1145\/380752.380757"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/1642724"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Ardeshir-Larijani E Gay SJ Nagarajan R (2014) Verification of concurrent quantum protocols by equivalence checking. In: Proceedings of the 20th international conference on tools and algorithms for the construction and analysis of systems (TACAS) pp 500\u2013514","DOI":"10.1007\/978-3-642-54862-8_42"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005299"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Barthe G Fournet C Gr\u00e9goire B Strub P-Y Swamy N Zanella B\u00e9guelin S (2014) Probabilistic relational verification for cryptographic implementations. In: Proceedings of the 41st annual ACM symposium on principles of programming languages (POPL) pp 193\u2013206","DOI":"10.1145\/2535838.2535847"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Barthe G K\u00f6pf B Olmedo F Zanella B\u00e9guelin Z (2013) Probabilistic relational reasoning for differential privacy. In: ACM transactions on programming languages and systems vol 35 No. 9","DOI":"10.1145\/2492061"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Chakarov A Sankaranarayanan S (2013) Probabilistic program analysis with martingales. In: Proceedings of the 25th international conference on computer aided verification (CAV). Springer LNCS 8044 pp 511\u2013526","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Chatterjee K Fu HF Novotn\u00fd P Hasheminezhad R (2016) Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Proceedings of the 43rd annual ACM symposium on principles of programming languages (POPL) pp 327\u2013342","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.56.1201"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Col\u00f3n MA Sankaranarayanan S Sipma HB (2003) Linear invariant generation using non-linear constraint solving. In: Proceedings of the 15th international conference on computer aided verification (CAV). Springer LNCS pp 420\u2013433","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","first-page":"8203","DOI":"10.1038\/ncomms9203","article-title":"Provable quantum advantage in randomness processing","volume":"6","author":"Dale H","year":"2015","journal-title":"Nat Commun"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Feng Y Hahn EM Turrini A Zhang LJ (2015) QPMC: a model checker for quantum programs and protocols. In: Proceedings of the 20th international symposium on formal methods (FM). Springer LNCS 9109 pp 265\u2013272","DOI":"10.1007\/978-3-319-19249-9_17"},{"key":"e_1_2_1_2_18_2","unstructured":"Feng Y Ying MS (2015) Toward automatic verification of quantum cryptographic protocols. In: Proceedings of the 26th international conference on concurrency theory (CONCUR) pp 441\u2013455"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2013.04.002"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Fioriti LMF Hermanns H (2015) Probabilistic termination: soundness completeness and compositionality. In: Proceedings of the 42nd annual ACM symposium on principles of programming languages (POPL) pp 489\u2013501","DOI":"10.1145\/2775051.2677001"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Gay SJ Papanikolaou N Nagarajan R (2008) QMC: a model checker for quantum systems. In: Proceedings of the 20th international conference on computer aided verification (CAV). Springer LNCS 5123 pp 543\u2013547","DOI":"10.1007\/978-3-540-70545-1_51"},{"key":"e_1_2_1_2_22_2","first-page":"885","article-title":"Measures on the closed subspaces of a Hilbert space","volume":"6","author":"Gleason AM","year":"1957","journal-title":"J Math Mech"},{"key":"e_1_2_1_2_23_2","unstructured":"Gorelick GA (1975) A complete axiomatic system for proving assertions about recursive and non-recursive programs. Technical Report Department of Computer Science University of Toronto"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Green A Lumsdaine PL Ross NJ Selinger P Valiron B (2013) Quipper: a scalable quantum programming language. In: Proceedings of the 34th ACM conference on programming language design and implementation (PLDI) pp 333\u2013342","DOI":"10.1145\/2499370.2462177"},{"key":"e_1_2_1_2_25_2","unstructured":"Grover LK (1997) Quantum telecomputation. arXiv:quant-ph\/9704012"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Harel D (1979) First-order dynamic logic LNCS 68. Springer","DOI":"10.1007\/3-540-09237-4"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200114X"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1007\/s001650050057","article-title":"Hoare logic and auxiliary variables","volume":"11","author":"Leymann T","year":"1999","journal-title":"Formal Asp Comput"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Katoen J-P McIver A Meinicke L Morgan CC (2010) Linear-invariant generation for probabilistic programs\u2014automated support for proof-based methods. In: Proceedings 17th international symposium on static analysis (SAS). Springer LNCS 6337 pp 390\u2013406","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2015.05.001"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.parco.2014.12.001"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Kakutani Y (2009) A logic for formal verification of quantum programs. In: Proceedings of the 13th Asian computing science conference (ASIAN 2009). Springer LNCS 5913 pp 79\u201393","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Li YJ Ying MS (2018) Algorithmic analysis of termination problems for quantum programs. In: Proceedings of the 45th annual ACM symposium on principles of programming languages (POPL) pp 35.1\u201335.29","DOI":"10.1145\/3158123"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-013-0185-3"},{"key":"e_1_2_1_2_35_2","unstructured":"Liu T Li YJ Wang SL et al A theorem prover for quantum Hoare logic and its applications. arXiv:1601.03835"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.5555\/1149028.1709607"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"van Meter R Munro WJ Nemoto K Itoh KM (2008) Arithmetic on a distributed-memory quantum multicomputer. ACM J Emerg Technol Comput Syst 3 Art. No. 17","DOI":"10.1145\/1324177.1324179"},{"key":"e_1_2_1_2_38_2","volume-title":"Abstraction, refinement and proof for probabilistic systems","author":"McIver A","year":"2005"},{"key":"e_1_2_1_2_39_2","volume-title":"Quantum computation and quantum information","author":"Nielsen MA","year":"2000"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Paykin J Rand R Zdancewic S (2017) QWIRE: a core language for quantum circuits. In: Proceedings of the 44th annual ACM symposium on principles of programming languages (POPL) pp 846\u2013858","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_2_1_2_41_2","unstructured":"Rand R Verification logics for quantum programs. http:\/\/www.cis.upenn.edu\/~rrand\/wpe.pdf"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S Sipma HB Manna Z (2004) Non-linear loop invariant generation using Gr\u00f6bner bases. In: Proceedings of the 31st ACM symposium on principles of programming languages (POPL) pp 318\u2013329","DOI":"10.1145\/964001.964028"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Serafini A Mancinians S Bose S (2006) Distributed quantum computation via optical fibers. Phys Rev Lett 96 Art. No. 010503","DOI":"10.1103\/PhysRevLett.96.010503"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Svore K Geller A Troyer M Azariah J Granade C Heim B Kliuchnikov V Mykhailova M Paz A Roetteler M (2018) Q#: enabling scalable quantum computing and development with a high-level DSL. In: Proceedings of the real world domain specific languages workshop 2018 Art. no. 8","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Tani S Kobayashi H Matsumoto K (2012) Exact quantum algorithms for the leader election problem. ACM Trans Comput Theory 4 Art. No. 1","DOI":"10.1145\/2141938.2141939"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1038\/nature09770"},{"key":"e_1_2_1_2_48_2","unstructured":"Unruh D Quantum relational Hoare logic. https:\/\/arxiv.org\/pdf\/1802.03188.pdf"},{"key":"e_1_2_1_2_49_2","unstructured":"Wecker D Svore KM (2014) LIQUi|>: a software design architecture and domain-specific language for quantum computing. arXiv:1402.4467"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Ying MS (2011) Floyd-Hoare logic for quantum programs. ACM Trans Program Lang Syst 39 Art. no. 19","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Ying MS (2016) Foundations of quantum programs. Morgan-Kaufmann","DOI":"10.1016\/B978-0-12-802306-8.00004-5"},{"key":"e_1_2_1_2_52_2","unstructured":"Ying MS (2016) Toward automatic verification of quantum programs (extended abstract). In: Proceedings of the 2nd international symposium on dependable software engineering: theories tools and applications (SETTA)"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2007.06.003"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-010-0117-4"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.94"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Ying MS Li YJ Yu NK Feng Y (2014) Model-checking linear-time properties of quantum systems. ACM Trans Comput Logic 15 Art. no. 22","DOI":"10.1145\/2629680"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Ying MS Ying SG Wu XD (2017) Invariants of quantum programs: characterisations and generation. In: Proceedings of the 44th annual ACM symposium on principles of programming languages (POPL) pp 818\u2013832","DOI":"10.1145\/3009837.3009840"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.016"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Ying SG Feng Y Yu NK Ying MS (2013) Reachability analysis of quantum Markov chains. In: Proceedings of the 24th Int Conf Concurr Theory (CONCUR) pp 334\u2013348","DOI":"10.1007\/978-3-642-40184-8_24"},{"key":"e_1_2_1_2_60_2","doi-asserted-by":"crossref","unstructured":"Yu NK Ying MS (2012) Reachability and termination analysis of concurrent quantum programs. In: Proceedings of the 23th international conference on concurrency theory (CONCUR) pp 69\u201383","DOI":"10.1007\/978-3-642-32940-1_7"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0465-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-018-0465-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-018-0465-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-018-0465-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:55:27Z","timestamp":1641538527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-018-0465-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,12]]},"references-count":60,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2,12]]}},"alternative-id":["10.1007\/s00165-018-0465-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-018-0465-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,2,12]]},"assertion":[{"value":"30 May 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 July 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 August 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}