{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:05Z","timestamp":1772164085383,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Key Research Program of Frontier Sciences, CAS"},{"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":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009840","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"818-832","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Invariants of quantum programs: characterisations and generation"],"prefix":"10.1145","author":[{"given":"Mingsheng","family":"Ying","sequence":"first","affiliation":[{"name":"University of Technology Sydney, Australia \/ Tsinghua University, China \/ Institute of Software at Chinese Academy of Sciences, China"}]},{"given":"Shenggang","family":"Ying","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia"}]},{"given":"Xiaodi","family":"Wu","sequence":"additional","affiliation":[{"name":"University of Oregon, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/380752.380758"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005299"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_3_2_1_9_1","first-page":"67","volume-title":"Synthesis of linear ranking functions","author":"Col\u00b4on M.","year":"2001","unstructured":"M. Col\u00b4on and H. Sipma , Synthesis of linear ranking functions , In : Proc. of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2001 , Springer LNCS 2031, pp. 67 - 81 . M. Col\u00b4on and H. Sipma, Synthesis of linear ranking functions, In: Proc. of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2001, Springer LNCS 2031, pp. 67-81."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_1_12_1","first-page":"200","volume":"52","author":"Derksen H.","year":"2005","unstructured":"H. Derksen and J. Weyman , Quiver representations, Notices of the American Mathematical Society , 52 ( 2005 ) 200 - 206 . H. Derksen and J. Weyman, Quiver representations, Notices of the American Mathematical Society, 52(2005)200-206.","journal-title":"Quiver representations, Notices of the American Mathematical Society"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.011"},{"key":"e_1_3_2_1_15_1","first-page":"1181","volume":"79","author":"Feng Y.","year":"2013","unstructured":"Y. Feng , N. K. Yu and M. S. Ying , Model checking quantum Markov chains, Journal of Computer and System Sciences , 79 ( 2013 ) 1181 - 1198 . Y. Feng, N. K. Yu and M. S. Ying, Model checking quantum Markov chains, Journal of Computer and System Sciences, 79(2013)1181- 1198.","journal-title":"Model checking quantum Markov chains, Journal of Computer and System Sciences"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005378"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_51"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1103\/RevModPhys.86.153"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1975.6312821"},{"key":"e_1_3_2_1_22_1","unstructured":"M. Grant and S. Boyd. CVX: Matlab software for disciplined convex programming version 2.0 beta. http:\/\/cvxr.com\/cvx September 2013.  M. Grant and S. Boyd. CVX: Matlab software for disciplined convex programming version 2.0 beta. http:\/\/cvxr.com\/cvx September 2013."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40196-1_17"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"S. Gudder Quantum Markov chains Journal of Mathematical Physics 49(2008) art. no. 072105.  S. Gudder Quantum Markov chains Journal of Mathematical Physics 49(2008) art. no. 072105.","DOI":"10.1063\/1.2953952"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"G. Gutoski and X. Wu Parallel approximation of min-max problems with applications to classical and quantum zero-sum games Computational Complexity 22(2013) 385-428.  G. Gutoski and X. Wu Parallel approximation of min-max problems with applications to classical and quantum zero-sum games Computational Complexity 22(2013) 385-428.","DOI":"10.1007\/s00037-013-0065-9"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.26"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_3_2_1_31_1","first-page":"390","volume-title":"Proc. 17th International Symposium on Static Analysis (SAS)","author":"Katoen J. -P.","year":"2010","unstructured":"J. -P. Katoen , A. McIver , L. Meinicke and C. C. Morgan , Linearinvariant generation for probabilistic programs - Automated support for proof-based methods , in: Proc. 17th International Symposium on Static Analysis (SAS) , 2010 , Springer LNCS 6337 , pp. 390 - 406 . J. -P. Katoen, A. McIver, L. Meinicke and C. C. Morgan, Linearinvariant generation for probabilistic programs - Automated support for proof-based methods, in: Proc. 17th International Symposium on Static Analysis (SAS), 2010, Springer LNCS 6337, pp. 390-406."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/360032.360048"},{"key":"e_1_3_2_1_33_1","first-page":"509","volume-title":"J. Barwise and S. Feferman (eds.)","author":"Keisler H. J.","year":"1985","unstructured":"H. J. Keisler , Probability quantifiers , In: J. Barwise and S. Feferman (eds.) , Model Theoretic Logics, Springer , 1985 , pp. 509 - 556 . H. J. Keisler, Probability quantifiers, In: J. Barwise and S. Feferman (eds.), Model Theoretic Logics, Springer, 1985, pp. 509-556."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(92)90132-F"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1036296"},{"key":"e_1_3_2_1_36_1","unstructured":"Y. J. Li T. Liu S. L. Wang N. J. Zhan and M. S. Ying A theorem prover for quantum Hoare logic and its applications http:\/\/arxiv.org\/pdf\/1601.03835.pdf  Y. J. Li T. Liu S. L. Wang N. J. Zhan and M. S. Ying A theorem prover for quantum Hoare logic and its applications http:\/\/arxiv.org\/pdf\/1601.03835.pdf"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535879"},{"key":"e_1_3_2_1_39_1","volume-title":"Many-Valued Logic","author":"Rescher N.","year":"1969","unstructured":"N. Rescher , Many-Valued Logic , McGraw-Hill , 1969 . N. Rescher, Many-Valued Logic, McGraw-Hill, 1969."},{"key":"e_1_3_2_1_40_1","first-page":"88","volume-title":"Proceedings of 5th International Conference on Mathematics of Program Construction (MPC), 2000","author":"Sanders J. W.","year":"1837","unstructured":"J. W. Sanders and P. Zuliani , Quantum programming , In: Proceedings of 5th International Conference on Mathematics of Program Construction (MPC), 2000 , Springer LNCS 1837 , Springer pp. 88 - 99 . J. W. Sanders and P. Zuliani, Quantum programming, In: Proceedings of 5th International Conference on Mathematics of Program Construction (MPC), 2000, Springer LNCS 1837, Springer pp. 88-99."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24754-8_1"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90194-M"},{"key":"e_1_3_2_1_45_1","unstructured":"Stanford Invariant Generator http:\/\/theory.stanford.edu\/ srirams\/Software\/sting.html.  Stanford Invariant Generator http:\/\/theory.stanford.edu\/ srirams\/Software\/sting.html."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676999"},{"key":"e_1_3_2_1_47_1","first-page":"87","volume":"471","author":"Temme K.","year":"2011","unstructured":"K. Temme , T. J. Osborne , K. G. Vollbrecht , D. Poulin , and F. Verstraete . Quantum Metropolis sampling. Nature , 471 ( 2011 ) 87 - 90 . K. Temme, T. J. Osborne, K. G. Vollbrecht, D. Poulin, and F. Verstraete. Quantum Metropolis sampling. Nature, 471(2011) 87-90.","journal-title":"Quantum Metropolis sampling. Nature"},{"key":"e_1_3_2_1_48_1","unstructured":"D. Wecker and K. M. Svore LIQUi |\u27e9: A software design architecture and domain-specific language for quantum computing http:\/\/research.microsoft.com\/pubs\/209634\/1402.4467.pdf.  D. Wecker and K. M. Svore LIQUi |\u27e9: A software design architecture and domain-specific language for quantum computing http:\/\/research.microsoft.com\/pubs\/209634\/1402.4467.pdf."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_1_50_1","volume-title":"Morgan-Kaufmann","author":"Ying M. S.","year":"2016","unstructured":"M. S. Ying , Foundations of Quantum Programming , Morgan-Kaufmann , 2016 . M. S. Ying, Foundations of Quantum Programming, Morgan-Kaufmann, 2016."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-010-0117-4"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629680"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.016"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009840","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009840","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:21Z","timestamp":1750203381000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009840"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":51,"alternative-id":["10.1145\/3009837.3009840","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009840","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009840","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}