{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:36:50Z","timestamp":1773193010382,"version":"3.50.1"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"8","license":[{"start":{"date-parts":[[2024,11,30]],"date-time":"2024-11-30T00:00:00Z","timestamp":1732924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["12271172, 11871221, 62472175 & 62072176"],"award-info":[{"award-number":["12271172, 11871221, 62472175 & 62072176"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100012166","name":"National Key R & D Program of China","doi-asserted-by":"crossref","award":["2018YFA0306704"],"award-info":[{"award-number":["2018YFA0306704"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"crossref","award":["2021JQRH014"],"award-info":[{"award-number":["2021JQRH014"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"crossref"}]},{"name":"\u201cDigital Silk Road\u201d Shanghai International Joint Lab of Trustworthy Intelligent Software","award":["22510750100"],"award-info":[{"award-number":["22510750100"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2024,11,30]]},"abstract":"<jats:p>\n            Verifying quantum programs has attracted a lot of interest in recent years. In this article, we consider the following two categories of termination problems of quantum programs with nondeterminism, namely:\n            <jats:list list-type=\"order\">\n              <jats:list-item>\n                <jats:label>(1)<\/jats:label>\n                <jats:p>(termination) Is an input of a program terminating with probability one under all schedulers? If not, how can a scheduler be synthesized to evidence the nontermination?<\/jats:p>\n              <\/jats:list-item>\n              <jats:list-item>\n                <jats:label>(2)<\/jats:label>\n                <jats:p>(universal termination) Are all inputs terminating with probability one under their respective schedulers? If yes, a further question asks whether there is a scheduler that forces all inputs to be terminating with probability one together with how to synthesize it; otherwise, how can an input be provided to refute the universal termination?<\/jats:p>\n              <\/jats:list-item>\n            <\/jats:list>\n          <\/jats:p>\n          <jats:p>\n            For the effective verification of the first category, we over-approximate the reachable set of quantum program states by the reachable subspace, whose algebraic structure is a linear space. On the other hand, we study the set of divergent states from which the program terminates with probability zero under\n            <jats:italic>some<\/jats:italic>\n            scheduler. The divergent set also has an explicit algebraic structure. Exploiting these explicit algebraic structures, we address the decision problem by a necessary and sufficient condition, i.e., the disjointness of the reachable subspace and the divergent set. Furthermore, the scheduler synthesis is completed in exponential time, whose bottleneck lies in computing the divergent set reported for the first time.\n          <\/jats:p>\n          <jats:p>\n            For the second category, we reduce the decision problem to the existence of an invariant subspace, from which the program terminates with probability zero under\n            <jats:italic>all<\/jats:italic>\n            schedulers. The invariant subspace is characterized by linear equations and thus can be efficiently computed. The states on that invariant subspace are evidence of the nontermination. Furthermore, the scheduler synthesis is completed by seeking a pattern of finite schedulers that forces all inputs to be terminating with positive probability. The repetition of that pattern yields the desired universal scheduler that forces all inputs to be terminating with probability one. All the problems in the second category are shown, also for the first time, to be solved in polynomial time. Finally, we demonstrate the aforementioned methods via a running example\u2014the quantum Bernoulli factory protocol.\n          <\/jats:p>","DOI":"10.1145\/3691632","type":"journal-article","created":{"date-parts":[[2024,9,2]],"date-time":"2024-09-02T15:09:04Z","timestamp":1725289744000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Termination and Universal Termination Problems for Nondeterministic Quantum Programs"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9906-5677","authenticated-orcid":false,"given":"Ming","family":"Xu","sequence":"first","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2367-9958","authenticated-orcid":false,"given":"Jianling","family":"Fu","sequence":"additional","affiliation":[{"name":"School of Computer Science and Technology, East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-4256-9508","authenticated-orcid":false,"given":"Hui","family":"Jiang","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0753-418X","authenticated-orcid":false,"given":"Yuxin","family":"Deng","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2534-8496","authenticated-orcid":false,"given":"Zhi-Bin","family":"Li","sequence":"additional","affiliation":[{"name":"School of Computer Science and Technology, East China Normal University, Shanghai, China"}]}],"member":"320","published-online":{"date-parts":[[2024,12,5]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"32","volume-title":"Proceedings of the ACM on Programming Languages","volume":"2","author":"Agrawal Sheshansh","year":"2018","unstructured":"Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotn\u00fd. 2018. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. Proceedings of the ACM on Programming Languages 2, POPL (2018), Article 34, 32 pages."},{"issue":"4","key":"e_1_3_2_3_2","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1145\/3512340","article-title":"When Software Engineering Meets Quantum Computing","volume":"65","author":"Ali Shaukat","year":"2022","unstructured":"Shaukat Ali, Tao Yue, and Rui Abreu. 2022. When Software Engineering Meets Quantum Computing. Communications of the ACM 65, 4 (2022), 84\u201388.","journal-title":"Communications of the ACM"},{"key":"e_1_3_2_4_2","first-page":"249","volume-title":"Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS \u201905)","author":"Altenkirch Thorsten","year":"2005","unstructured":"Thorsten Altenkirch and Jonathan Grattage. 2005. A Functional Quantum Programming Language. In Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS \u201905). IEEE Computer Society, 249\u2013258."},{"key":"e_1_3_2_5_2","first-page":"13","volume-title":"Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201922)","author":"Avanzini Martin","year":"2022","unstructured":"Martin Avanzini, Georg Moser, Romain P\u00e9choux, Simon Perdrix, and Vladimir Zamdzhiev. 2022. Quantum Expectation Transformers for Cost Analysis. In Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201922). Christel Baier and Dana Fisman (Eds.), ACM, New York, NY, Article 10, 13 pages."},{"key":"e_1_3_2_6_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press, Cambridge, MA."},{"key":"e_1_3_2_7_2","first-page":"117","volume-title":"Proceedings of the 27th European Symposium on Programming (ESOP \u201918), the European Joint Conferences on Theory and Practice of Software (ETAPS \u201918)","volume":"10801","author":"Barthe Gilles","year":"2018","unstructured":"Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. 2018. An Assertion-Based Program Logic for Probabilistic Programs. In Proceedings of the 27th European Symposium on Programming (ESOP \u201918), the European Joint Conferences on Theory and Practice of Software (ETAPS \u201918). Amal Ahmed (Ed.), LNCS, Vol. 10801, Springer, Berlin, 117\u2013144."},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry","author":"Basu Saugata","year":"2006","unstructured":"Saugata Basu, Richard Pollack, and Marie-Fran\u00e7oise Roy. 2006. Algorithms in Real Algebraic Geometry (2nd ed.). Springer, Berlin.","edition":"2"},{"key":"e_1_3_2_9_2","first-page":"2792","volume-title":"Proceedings of the ACM on Programming Languages 8","author":"Batz Kevin","year":"2024","unstructured":"Kevin Batz, Tom J. Biskup, Joost-Pieter Katoen, and Tobias Winkler. 2024. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs. Proceedings of the ACM on Programming Languages 8, POPL (2024), 2792\u20132820."},{"issue":"4","key":"e_1_3_2_10_2","first-page":"55","article-title":"Ranking Functions for Linear-Constraint Loops","volume":"61","author":"Ben-Amram Amir M.","year":"2014","unstructured":"Amir M. Ben-Amram and Samir Genaim. 2014. Ranking Functions for Linear-Constraint Loops. Journal of the ACM 61, 4 (2014), Article 26, 55 pages.","journal-title":"Journal of the ACM"},{"key":"e_1_3_2_11_2","first-page":"511","volume-title":"Proceedings of the 25th International Conference, (CAV \u201913)","volume":"8044","author":"Chakarov Aleksandar","year":"2013","unstructured":"Aleksandar Chakarov and Sleksandar Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Proceedings of the 25th International Conference, (CAV \u201913). Natasha Sharygina and Helmut Veith (Eds.), LNCS, Vol. 8044, Springer, Berlin, 511\u2013526."},{"key":"e_1_3_2_12_2","first-page":"3","volume-title":"Computer Aided Verification, Proceedings of the 28th International Conference on Computer Aided Verification (CAV \u201916)","volume":"9779","author":"Chatterjee Krishnendu","year":"2016","unstructured":"Krishnendu Chatterjee, Hongfei Fu, and Amir K. Goharshady. 2016. Termination Analysis of Probabilistic Programs through Positivstellensatz\u2019s. In Computer Aided Verification, Proceedings of the 28th International Conference on Computer Aided Verification (CAV \u201916). Swarat Chaudhuri and Azadeh Farzan (Eds.), LNCS, Vol. 9779, Springer, Berlin, 3\u201322."},{"key":"e_1_3_2_13_2","doi-asserted-by":"crossref","first-page":"3408","DOI":"10.1103\/PhysRevLett.80.3408","article-title":"Experimental Implementation of Fast Quantum Searching","volume":"80","author":"Chuang Isaac L.","year":"1998","unstructured":"Isaac L. Chuang, Neil A. Gershenfeld, and Mark Kubinec. 1998. Experimental Implementation of Fast Quantum Searching. Physical Review Letters 80 (1998), 3408\u20133411.","journal-title":"Physical Review Letters"},{"issue":"2","key":"e_1_3_2_14_2","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications","volume":"8","author":"Clarke E. M.","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. 1986. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8, 2 (1986), 244\u2013263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_2_15_2","first-page":"238","volume-title":"Proceedings of the 4th ACM Symposium on Principles of Programming Languages","author":"Cousot Patrick","year":"1977","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Robert M. Graham, Michael A. Harrison, and Ravi Sethi (Eds.). ACM, New York, 238\u2013252."},{"key":"e_1_3_2_16_2","first-page":"592","volume-title":"Proceedings of the 29th International Conference on Computer Aided Verification (CAV \u201917)","author":"Dehnert Christian","year":"2017","unstructured":"Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. 2017. A Storm is Coming: A Modern Probabilistic Model Checker. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV \u201917). Rupak Majumdar and Viktor Kuncak (Eds.), Springer, Berlin, 592\u2013600."},{"issue":"3","key":"e_1_3_2_17_2","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1017\/S0960129506005251","article-title":"Quantum Weakest Preconditions","volume":"16","author":"D\u2019Hondt Ellie","year":"2006","unstructured":"Ellie D\u2019Hondt and Prakash Panangaden. 2006. Quantum Weakest Preconditions. Mathematical Structures in Computer Science 16, 3 (2006), 429\u2013451.","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_3_2_18_2","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall, New York."},{"key":"e_1_3_2_19_2","first-page":"1040","volume-title":"Proceedings of the ACM on Programming Languages 8","author":"Fang Wang","year":"2024","unstructured":"Wang Fang and Mingsheng Ying. 2024. Symbolic Execution for Quantum Error Correction Programs. Proceedings of the ACM on Programming Languages 8, PLDI (2024), 1040\u20131065."},{"issue":"1","key":"e_1_3_2_20_2","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/j.tcs.2007.06.011","article-title":"Proof Rules for the Correctness of Quantum Programs","volume":"386","author":"Feng Yuan","year":"2007","unstructured":"Yuan Feng, Runyao Duan, Zheng-Feng Ji, and Mingsheng Ying. 2007. Proof Rules for the Correctness of Quantum Programs. Theoretical Computer Science 386, 1\u20132 (2007), 151\u2013166.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_2_21_2","first-page":"22","article-title":"Abstract Interpretation, Hoare Logic, and Incorrectness Logic for Quantum Programs","volume":"294","author":"Feng Yuan","year":"2023","unstructured":"Yuan Feng and Sanjiang Li. 2023. Abstract Interpretation, Hoare Logic, and Incorrectness Logic for Quantum Programs. Information and Computation 294 (2023), Article 105077, 22 pages.","journal-title":"Information and Computation"},{"key":"e_1_3_2_22_2","first-page":"789","volume-title":"Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","volume":"3","author":"Feng Yuan","year":"2023","unstructured":"Yuan Feng and Yingte Xu. 2023. Verification of Nondeterministic Quantum Programs. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Vol. 3. Tor M. Aamodt, Natalie D. Enright Jerger, and Michael M. Swift (Eds.), ACM, New York, NY, 789\u2013805."},{"issue":"4","key":"e_1_3_2_23_2","first-page":"43","article-title":"Quantum Hoare Logic with Classical Variables","volume":"2","author":"Feng Yuan","year":"2021","unstructured":"Yuan Feng and Mingsheng Ying. 2021. Quantum Hoare Logic with Classical Variables. ACM Transactions on Quantum Computing 2, 4, Article 16 (2021), 43 pages.","journal-title":"ACM Transactions on Quantum Computing"},{"issue":"7","key":"e_1_3_2_24_2","doi-asserted-by":"crossref","first-page":"1181","DOI":"10.1016\/j.jcss.2013.04.002","article-title":"Model Checking Quantum Markov Chains.","volume":"79","author":"Feng Yuan","year":"2013","unstructured":"Yuan Feng, Nengkun Yu, and Mingsheng Ying. 2013. Model Checking Quantum Markov Chains. Journal of Computer and System Sciences 79, 7 (2013), 1181\u20131198.","journal-title":"Journal of Computer and System Sciences"},{"key":"e_1_3_2_25_2","first-page":"489","volume-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915).","author":"Fioriti Luis M. F.","year":"2015","unstructured":"Luis M. F. Fioriti and Holger Hermanns. 2015. Probabilistic Termination: Soundness, Completeness, and Compositionality. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201915). Sriram. K. Rajamani and David Walker (Eds.), ACM, New York, NY, 489\u2013501."},{"key":"e_1_3_2_26_2","first-page":"468","volume-title":"Verification, Model Checking, and Abstract Interpretation - Proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI \u201919)","volume":"11388","author":"Fu Hongfei","year":"2019","unstructured":"Hongfei Fu and Krishnendu Chatterjee. 2019. Termination of Nondeterministic Probabilistic Programs. In Verification, Model Checking, and Abstract Interpretation - Proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI \u201919). Constantin Enea and Ruzica Piskac (Eds.), LNCS, Vol. 11388, Springer, Berlin, 468\u2013490."},{"key":"e_1_3_2_27_2","unstructured":"Google. 2018. Cirq: A Python Library for Writing Manipulating and Optimizing Quantum Circuits and Running Them against Quantum Computers and Simulators. Retrieved from https:\/\/github.com\/quantumlib\/Cirq"},{"key":"e_1_3_2_28_2","first-page":"533","volume-title":"Proceedings of the 36th International Conference on Computer Aided Verification (CAV \u201924)","volume":"14683","author":"Guan Ji","year":"2024","unstructured":"Ji Guan, Yuan Feng, Andrea Turrini, and Mingsheng Ying. 2024. Measurement-Based Verification of Quantum Markov Chains. In Proceedings of the 36th International Conference on Computer Aided Verification (CAV \u201924). Arie Gurfinkel and Vijay Ganesh (Eds.), LNCS, Vol. 14683, Springer, Berlin, 533\u2013554."},{"issue":"2","key":"e_1_3_2_29_2","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/S0167-6423(96)00019-6","article-title":"Probabilistic Models for the Guarded Command Language","volume":"28","author":"He Jifeng","year":"1997","unstructured":"Jifeng He, Karen Seidel, and Annabelle McIver. 1997. Probabilistic Models for the Guarded Command Language. Science of Computer Programming 28, 2\u20133 (1997), 171\u2013192.","journal-title":"Science of Computer Programming"},{"key":"e_1_3_2_30_2","first-page":"162","volume-title":"Proceedings of the IEEE International Conference on Quantum Software (QSW)","author":"Herrmann Nils","year":"2023","unstructured":"Nils Herrmann, Daanish Arya, Marcus W. Doherty, Angus Mingare, Jason C. Pillay, Florian Preis, and Stefan Prestel. 2023. Quantum Utility\u2014Definition and Assessment of a Practical Quantum Advantage. In Proceedings of the IEEE International Conference on Quantum Software (QSW). IEEE Computer Society, 162\u2013174."},{"key":"e_1_3_2_31_2","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Communications of the ACM 12 10 (1969) 576\u2013580.","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_32_2","unstructured":"IBM. 2020. Qiskit: An Open-Source SDK for Working with Quantum Computers at the Level of Pulses Circuits and Algorithms. Retrieved from https:\/\/github.com\/QISKit"},{"key":"e_1_3_2_33_2","unstructured":"IBM. 2023. IBM Debuts Next-Generation Quantum Processor & IBM Quantum System Two Extends Roadmap to Advance Era of Quantum Utility. Retrieved from https:\/\/newsroom.ibm.com\/"},{"key":"e_1_3_2_34_2","volume-title":"Fixed Point Theory: An Introduction","author":"Istr\u01ce\u0163escu Vasile I.","year":"2001","unstructured":"Vasile I. Istr\u01ce\u0163escu. 2001. Fixed Point Theory: An Introduction. Springer, Berlin."},{"key":"e_1_3_2_35_2","first-page":"12","volume-title":"Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control (HSCC \u201924).","author":"Jiang Hui","year":"2024","unstructured":"Hui Jiang, Jianling Fu, Ming Xu, Yuxin Deng, and Zhi-Bin Li. 2024. A Sample-Driven Solving Procedure for the Repeated Reachability of Quantum Continuous-Time Markov Chains. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control (HSCC \u201924). ACM, New York, NY, Article 9, 12 pages."},{"issue":"3","key":"e_1_3_2_36_2","first-page":"6","article-title":"Quantum-to-Quantum Bernoulli Factory Problem","volume":"97","author":"Jiang Jiaqing","year":"2018","unstructured":"Jiaqing Jiang, Jialin Zhang, and Xiaoming Sun. 2018. Quantum-to-Quantum Bernoulli Factory Problem. Physical Review A 97, 3 (2018), Article 032303, 6 pages.","journal-title":"Physical Review A"},{"key":"e_1_3_2_37_2","first-page":"52","article-title":"Quantum Walk and Its Application Domains: A Systematic Review","volume":"41","author":"Kadian Karuna","year":"2021","unstructured":"Karuna Kadian, Sunita Garhwal, and Ajay Kumar. 2021. Quantum Walk and Its Application Domains: A Systematic Review. Computer Science Review 41 (2021), Article 100419, 52 pages.","journal-title":"Computer Science Review"},{"key":"e_1_3_2_38_2","first-page":"307","volume-title":"Proceedings of the 40th International Symposium on Mathematical Foundations of Computer Science (MFCS \u201915)","volume":"9234","author":"Kaminski Benjamin L.","year":"2015","unstructured":"Benjamin L. Kaminski and Joost-Pieter Katoen. 2015. On the Hardness of Almost-Sure Termination. In Proceedings of the 40th International Symposium on Mathematical Foundations of Computer Science (MFCS \u201915). Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella (Eds.), LNCS, Vol. 9234, Springer, Berlin, 307\u2013318."},{"key":"e_1_3_2_39_2","first-page":"364","volume-title":"Proceedings of the 25th European Symposium on Programming (ESOP \u201916)","author":"Kaminski Benjamin L.","year":"2016","unstructured":"Benjamin L. Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In Proceedings of the 25th European Symposium on Programming (ESOP \u201916). Peter Thiemann (Ed.), LNCS, Vol. 9632, Springer, Berlin, 364\u2013389."},{"issue":"5","key":"e_1_3_2_40_2","first-page":"68","article-title":"Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms","volume":"65","author":"Kaminski Benjamin L.","year":"2018","unstructured":"Benjamin L. Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. Journal of the ACM 65, 5 (2018), Article 30, 68 pages.","journal-title":"Journal of the ACM"},{"key":"e_1_3_2_41_2","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-319-23506-6_4","volume-title":"Correct System Design","author":"Katoen Joost-Pieter","year":"2015","unstructured":"Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin L. Kaminski, and Federico Olmedo. 2015. Understanding Probabilistic Programs. In Correct System Design. Roland Meyer, Andr\u00e9 Platzer, and Heike Wehrheim (Eds.), LNCS, Vol. 9360, Springer, Berlin, 15\u201332."},{"issue":"2","key":"e_1_3_2_42_2","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/175007.175019","article-title":"A Bernoulli Factory","volume":"4","author":"Keane M. S.","year":"1994","unstructured":"M. S. Keane and George L. O\u2019Brien. 1994. A Bernoulli Factory. ACM Transactions on Modeling and Computer Simulation 4, 2 (1994), 213\u2013219.","journal-title":"ACM Transactions on Modeling and Computer Simulation"},{"key":"e_1_3_2_43_2","first-page":"101","volume-title":"Proceedings of the 20th Annual Symposium on Foundations of Computer Science","author":"Kozen Dexter","year":"1979","unstructured":"Dexter Kozen. 1979. Semantics of Probabilistic Programs. In Proceedings of the 20th Annual Symposium on Foundations of Computer Science. IEEE Computer Society, 101\u2013114."},{"key":"e_1_3_2_44_2","first-page":"291","volume-title":"Proceedings of the 15th Annual ACM Symposium on Theory of Computing","author":"Kozen Dexter","year":"1983","unstructured":"Dexter Kozen. 1983. A Probabilistic PDL. In Proceedings of the 15th Annual ACM Symposium on Theory of Computing. David S. Johnson, Ronald Fagin, Michael L. Fredman, David Harel, Richard M. Karp, Nancy A. Lynch, Christos H. Papadimitriou, Ronald L. Rivest, Walter L. Ruzzo, and Joel I. Seiferas (Eds.). ACM, New York, NY, 291\u2013297."},{"key":"e_1_3_2_45_2","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification: Proceedings of the 23rd International Conference on Computer Aided Verification (CAV \u201911)","volume":"6806","author":"Kwiatkowska Marta","year":"2011","unstructured":"Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In Computer Aided Verification: Proceedings of the 23rd International Conference on Computer Aided Verification (CAV \u201911). Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), LNCS, Vol. 6806, Springer, Berlin, 585\u2013591."},{"issue":"1","key":"e_1_3_2_46_2","first-page":"35","article-title":"Formal Verification of Quantum Programs: Theory, Tools, and Challenges","volume":"5","author":"Lewis Marco","year":"2023","unstructured":"Marco Lewis, Sadegh Soudjani, and Paolo Zuliani. 2023. Formal Verification of Quantum Programs: Theory, Tools, and Challenges. ACM Transactions on Quantum Computing 5, 1 (2023), Article 1, 35 pages.","journal-title":"ACM Transactions on Quantum Computing"},{"key":"e_1_3_2_47_2","first-page":"29","volume-title":"Proceedings of the ACM on Programming Languages 2","author":"Li Yangjia","year":"2018","unstructured":"Yangjia Li and Mingsheng Ying. 2018. Algorithmic Analysis of Termination Problems for Quantum Programs. Proceedings of the ACM on Programming Languages 2, POPL (2018), Article 35, 29 pages."},{"issue":"1","key":"e_1_3_2_48_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s00236-013-0185-3","article-title":"Termination of Nondeterministic Quantum Programs","volume":"51","author":"Li Yangjia","year":"2014","unstructured":"Yangjia Li, Nengkun Yu, and Mingsheng Ying. 2014. Termination of Nondeterministic Quantum Programs. Acta Informatica 51, 1 (2014), 1\u201324.","journal-title":"Acta Informatica"},{"key":"e_1_3_2_49_2","first-page":"187","volume-title":"Proceedings of the 31st International Conference on Computer Aided Verification (CAV \u201919)","volume":"11562","author":"Liu Junyi","year":"2019","unstructured":"Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. 2019. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV \u201919). Isil Dillig and Serdar Tasiran (Eds.), LNCS, Vol. 11562, Springer, Berlin, 187\u2013207."},{"key":"e_1_3_2_50_2","first-page":"13","volume-title":"Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201922)","author":"Liu Junyi","year":"2022","unstructured":"Junyi Liu, Li Zhou, Gilles Barthe, and Mingsheng Ying. 2022. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. In Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201922). Christel Baier and Dana Fisman (Eds.), ACM, New York, NY, Article 4, 13 pages."},{"key":"e_1_3_2_51_2","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","year":"2006","unstructured":"Annabelle McIver and Carroll Morgan. 2006. Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Berlin."},{"key":"e_1_3_2_52_2","first-page":"28","volume-title":"Proceedings of the ACM on Programming Languages 2","author":"McIver Annabelle","year":"2018","unstructured":"Annabelle McIver, Carroll Morgan, Benjamin L. Kaminski, and Joost-Pieter Katoen. 2018. A New Proof Rule for Almost-Sure Termination. Proceedings of the ACM on Programming Languages 2, POPL (2018), Article 33, 28 pages."},{"key":"e_1_3_2_53_2","first-page":"491","volume-title":"Proceedings of the 30th European Symposium on Programming (ESOP \u201921)","author":"Moosbrugger Marcel","year":"2021","unstructured":"Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, and Laura Kov\u00e1cs. 2021. Automated Termination Analysis of Polynomial Probabilistic Programs. In Proceedings of the 30th European Symposium on Programming (ESOP \u201921). Nobuko Yoshida (Ed.), LNCS, Vol. 12648, Springer, Berlin, 491\u2013518."},{"issue":"3","key":"e_1_3_2_54_2","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1145\/229542.229547","article-title":"Probabilistic Predicate Transformers","volume":"18","author":"Morgan Carroll","year":"1996","unstructured":"Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. ACM Transactions on Programming Languages and Systems 18, 3 (1996), 325\u2013353.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"5","key":"e_1_3_2_55_2","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","article-title":"Computing Polynomial Program Invariants","volume":"91","author":"M\u00fcller-Olm Markus","year":"2004","unstructured":"Markus M\u00fcller-Olm and Helmut Seidl. 2004. Computing Polynomial Program Invariants. Information Processing Letters 91, 5 (2004), 233\u2013244.","journal-title":"Information Processing Letters"},{"key":"e_1_3_2_56_2","unstructured":"Juan M. Murillo Jos\u00e9 Garc\u00eda-Alonso Enrique Moguel Johanna Barzen Frank Leymann Shaukat Ali Tao Yue Paolo Arcaini Ricardo P\u00e9rez Ignacio G. R. de Guzm\u00e1n Mario Piattini Antonio Ruiz-Cort\u00e9s Antonio Brogi Jianjun Zhao Andriy V. Miranskyy and Manuel Wimmer. 2024. Challenges of quantum software engineering for the next decade: The road ahead. arXiv:2404.06825. Retrieved from https:\/\/arxiv.org\/abs\/2404.06825"},{"key":"e_1_3_2_57_2","volume-title":"Quantum Computation and Quantum Information","author":"Nielsen Michael A.","year":"2000","unstructured":"Michael A. Nielsen and Isaac L. Chuang. 2000. Quantum Computation and Quantum Information. Cambridge University Press, London."},{"key":"e_1_3_2_58_2","volume-title":"A Procedural Formalism for Quantum Computing","author":"\u00d6mer Bernhard","year":"1998","unstructured":"Bernhard \u00d6mer. 1998. A Procedural Formalism for Quantum Computing. Technical Report. Technical University of Vienna."},{"key":"e_1_3_2_59_2","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1007\/10722010_6","volume-title":"Mathematics of Program Construction","author":"Sanders Jeff W.","year":"2000","unstructured":"Jeff W. Sanders and Paolo Zuliani. 2000. Quantum Programming. In Mathematics of Program Construction. R. Backhouse and J. N. Oliveira (Eds.), Springer, Berlin, 80\u201399."},{"issue":"4","key":"e_1_3_2_60_2","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1017\/S0960129504004256","article-title":"Towards a Quantum Programming Language","volume":"14","author":"Selinger Peter","year":"2004","unstructured":"Peter Selinger. 2004. Towards a Quantum Programming Language. Mathematical Structures in Computer Science 14, 4 (2004), 527\u2013586.","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_3_2_61_2","first-page":"10","volume-title":"Proceedings of the Real World Domain Specific Languages Workshop (RWDSL@CGO \u201918)","author":"Svore Krysta","year":"2018","unstructured":"Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. 2018. Q#: Enabling Scalable Quantum Computing and Development with a High-level DSL. In Proceedings of the Real World Domain Specific Languages Workshop (RWDSL@CGO \u201918). ACM, New York, NY, Article 7, 10 pages."},{"key":"e_1_3_2_62_2","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.tcs.2022.08.016","article-title":"An Algebraic Method to Fidelity-Oriented Model Checking over Quantum Markov Chains","volume":"935","author":"Xu Ming","year":"2022","unstructured":"Ming Xu, Jianling Fu, Jingyi Mei, and Yuxin Deng. 2022. An Algebraic Method to Fidelity-Oriented Model Checking over Quantum Markov Chains. Theoretical Computer Science 935 (2022), 61\u201381.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_2_63_2","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.tcs.2022.01.044","article-title":"Model Checking QCTL Plus on Quantum Markov Chains","volume":"913","author":"Xu Ming","year":"2022","unstructured":"Ming Xu, Jianling Fu, Jingyi Mei, and Yuxin Deng. 2022. Model Checking QCTL Plus on Quantum Markov Chains. Theoretical Computer Science 913 (2022), 43\u201372.","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"e_1_3_2_64_2","doi-asserted-by":"crossref","first-page":"653","DOI":"10.1007\/s00236-020-00392-5","article-title":"Measuring the Constrained Reachability in Quantum Markov Chains","volume":"58","author":"Xu Ming","year":"2021","unstructured":"Ming Xu, Cheng-Chao Huang, and Yuan Feng. 2021. Measuring the Constrained Reachability in Quantum Markov Chains. Acta Informatica 58, 6 (2021), 653\u2013674.","journal-title":"Acta Informatica"},{"issue":"6","key":"e_1_3_2_65_2","first-page":"49","article-title":"Floyd\u2013Hoare Logic for Quantum Programs","volume":"33","author":"Ying Mingsheng","year":"2011","unstructured":"Mingsheng Ying. 2011. Floyd\u2013Hoare Logic for Quantum Programs. ACM Transactions on Programming Languages and Systems 33, 6 (2011), Article 19, 49 pages.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"e_1_3_2_66_2","volume-title":"Foundations of Quantum Programming","author":"Ying Mingsheng","year":"2016","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan Kaufmann, Amsterdam."},{"issue":"1","key":"e_1_3_2_67_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s00165-018-0465-3","article-title":"Toward Automatic Verification of Quantum Programs","volume":"31","author":"Ying Mingsheng","year":"2019","unstructured":"Mingsheng Ying. 2019. Toward Automatic Verification of Quantum Programs. Formal Aspects of Computing 31, 1 (2019), 3\u201325.","journal-title":"Formal Aspects of Computing"},{"key":"e_1_3_2_68_2","first-page":"311","article-title":"Predicate Transformer Semantics of Quantum Programs","volume":"8","author":"Ying Mingsheng","year":"2010","unstructured":"Mingsheng Ying, Runyao Duan, Yuan Feng, and Zhengfeng Ji. 2010. Predicate Transformer Semantics of Quantum Programs. Semantic Techniques in Quantum Computation 8 (2010), 311\u2013360.","journal-title":"Semantic Techniques in Quantum Computation"},{"issue":"4","key":"e_1_3_2_69_2","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/s00236-010-0117-4","article-title":"Quantum Loop Programs","volume":"47","author":"Ying Mingsheng","year":"2010","unstructured":"Mingsheng Ying and Yuan Feng. 2010. Quantum Loop Programs. Acta Informatica 47, 4 (2010), 221\u2013250.","journal-title":"Acta Informatica"},{"key":"e_1_3_2_70_2","doi-asserted-by":"crossref","first-page":"818","DOI":"10.1145\/3009837.3009840","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL \u201917).","author":"Ying Mingsheng","year":"2017","unstructured":"Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. 2017. Invariants of Quantum Programs: Characterisations and Generation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL \u201917).Giuseppe Castagna and Andrew D. Gordon (Eds.), ACM, New York, NY, 818\u2013832."},{"issue":"9","key":"e_1_3_2_71_2","doi-asserted-by":"crossref","first-page":"1679","DOI":"10.1016\/j.scico.2013.03.016","article-title":"Verification of Quantum Programs","volume":"78","author":"Ying Mingsheng","year":"2013","unstructured":"Mingsheng Ying, Nengkun Yu, Yuan Feng, and Runyao Duan. 2013. Verification of Quantum Programs. Science of Computer Programming 78, 9 (2013), 1679\u20131700.","journal-title":"Science of Computer Programming"},{"key":"e_1_3_2_72_2","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/j.ic.2018.09.001","article-title":"Reachability Analysis of Quantum Markov Decision Processes","volume":"263","author":"Ying Shenggang","year":"2018","unstructured":"Shenggang Ying and Mingsheng Ying. 2018. Reachability Analysis of Quantum Markov Decision Processes. Information and Computation 263 (2018), 31\u201351.","journal-title":"Information and Computation"},{"key":"e_1_3_2_73_2","first-page":"542","volume-title":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI \u201921)","author":"Yu Nengkun","year":"2021","unstructured":"Nengkun Yu and Jens Palsberg. 2021. Quantum Abstract Interpretation. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI \u201921). Stephen N. Freund and Eran Yahav (Eds.), ACM, New York, NY, 542\u2013558."},{"key":"e_1_3_2_74_2","first-page":"69","volume-title":"Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR \u201912)","volume":"7454","author":"Yu Nengkun","year":"2012","unstructured":"Nengkun Yu and Mingsheng Ying. 2012. Reachability and Termination Analysis of Concurrent Quantum Programs. In Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR \u201912). Maciej Koutny and Irek Ulidowski (Eds.), LNCS, Vol. 7454, Springer, Berlin, 69\u201383."},{"issue":"6523","key":"e_1_3_2_75_2","doi-asserted-by":"crossref","first-page":"1460","DOI":"10.1126\/science.abe8770","article-title":"Quantum Computational Advantage Using Photons","volume":"370","author":"Zhong Han-Sen","year":"2020","unstructured":"Han-Sen Zhong, Hui Wang, Yu-Hao Deng, Ming-Cheng Chen, Li-Chao Peng, Yi-Han Luo, Jian Qin, Dian Wu, Xing Ding, Yi Hu, Peng Hu, Xiao-Yan Yang, Wei-Jun Zhang, Hao Li, Yuxuan Li, Xiao Jiang, Lin Gan, Guangwen Yang, Lixing You, Zhen Wang, Li Li, Nai-Le Liu, Chao-Yang Lu, and Jian-Wei Pan. 2020. Quantum Computational Advantage Using Photons. Science 370, 6523 (2020), 1460\u20131463.","journal-title":"Science"},{"key":"e_1_3_2_76_2","first-page":"179","volume-title":"Proceedings of the 2nd International Workshop on Quantum Programming Languages","author":"Zuliani Paolo","year":"2004","unstructured":"Paolo Zuliani. 2004. Non-Deterministic Quantum Programming. In Proceedings of the 2nd International Workshop on Quantum Programming Languages. Turku Centre for Computer Science, Turku, 179\u2013195."}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3691632","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3691632","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:09:40Z","timestamp":1750295380000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3691632"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,30]]},"references-count":75,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2024,11,30]]}},"alternative-id":["10.1145\/3691632"],"URL":"https:\/\/doi.org\/10.1145\/3691632","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,30]]},"assertion":[{"value":"2024-04-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-21","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}