{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:05:15Z","timestamp":1767927915362,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,8,2]],"date-time":"2022-08-02T00:00:00Z","timestamp":1659398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2018YFA0306701"],"award-info":[{"award-number":["2018YFA0306701"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61832015"],"award-info":[{"award-number":["61832015"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,8,2]]},"DOI":"10.1145\/3531130.3533327","type":"proceedings-article","created":{"date-parts":[[2022,8,4]],"date-time":"2022-08-04T20:23:38Z","timestamp":1659644618000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs"],"prefix":"10.1145","author":[{"given":"Junyi","family":"Liu","sequence":"first","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, China and University of Chinese Academy of Sciences, China"}]},{"given":"Li","family":"Zhou","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Security and Privacy, Germany"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Security and Privacy, Germany and IMDEA Software Institute, Spain"}]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences, China and Tsinghua University, China"}]}],"member":"320","published-online":{"date-parts":[[2022,8,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/380752.380758"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539705447311"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77566-9_1"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/380752.380757"},{"key":"e_1_3_2_1_5_1","volume-title":"Quantum supremacy using a programmable superconducting processor. Nature 574, 7779","author":"Arute Frank","year":"2019","unstructured":"Frank Arute , Kunal Arya , Ryan Babbush , Dave Bacon , Joseph\u00a0 C Bardin , Rami Barends , Rupak Biswas , Sergio Boixo , Fernando\u00a0 GSL Brandao , David\u00a0 A Buell , 2019. Quantum supremacy using a programmable superconducting processor. Nature 574, 7779 ( 2019 ), 505\u2013510. https:\/\/doi.org\/10.1038\/s41586-019-1666-5 10.1038\/s41586-019-1666-5 Frank Arute, Kunal Arya, Ryan Babbush, Dave Bacon, Joseph\u00a0C Bardin, Rami Barends, Rupak Biswas, Sergio Boixo, Fernando\u00a0GSL Brandao, David\u00a0A Buell, 2019. Quantum supremacy using a programmable superconducting processor. Nature 574, 7779 (2019), 505\u2013510. https:\/\/doi.org\/10.1038\/s41586-019-1666-5"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_7"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.06.005"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_4"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11526841_9"},{"key":"e_1_3_2_1_10_1","volume-title":"European Symposium on Programming Languages and Systems. Springer, Springer Berlin Heidelberg, 105\u2013131","author":"\u010cern\u1ef3 Pavol","year":"2015","unstructured":"Pavol \u010cern\u1ef3 , Thomas\u00a0 A Henzinger , Laura Kov\u00e1cs , Arjun Radhakrishna , and Jakob Zwirchmayr . 2015 . Segment abstraction for worst-case execution time analysis . In European Symposium on Programming Languages and Systems. Springer, Springer Berlin Heidelberg, 105\u2013131 . https:\/\/doi.org\/10.1007\/978-3-662-46669-8_5 10.1007\/978-3-662-46669-8_5 Pavol \u010cern\u1ef3, Thomas\u00a0A Henzinger, Laura Kov\u00e1cs, Arjun Radhakrishna, and Jakob Zwirchmayr. 2015. Segment abstraction for worst-case execution time analysis. In European Symposium on Programming Languages and Systems. Springer, Springer Berlin Heidelberg, 105\u2013131. https:\/\/doi.org\/10.1007\/978-3-662-46669-8_5"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_6"},{"key":"e_1_3_2_1_13_1","volume-title":"APS March Meeting Abstracts, Vol.\u00a02018","author":"Cross Andrew","year":"2018","unstructured":"Andrew Cross . 2018 . The IBM Q experience and QISKit open-source quantum computing software . In APS March Meeting Abstracts, Vol.\u00a02018 . L58\u2013003. Andrew Cross. 2018. The IBM Q experience and QISKit open-source quantum computing software. In APS March Meeting Abstracts, Vol.\u00a02018. L58\u2013003."},{"key":"#cr-split#-e_1_3_2_1_14_1.1","doi-asserted-by":"crossref","unstructured":"Howard Dale David Jennings and Terry Rudolph. 2015. Provable quantum advantage in randomness processing. Nature communications 6(2015) 8203. https:\/\/doi.org\/10.1038\/ncomms9203 10.1038\/ncomms9203","DOI":"10.1038\/ncomms9203"},{"key":"#cr-split#-e_1_3_2_1_14_1.2","doi-asserted-by":"crossref","unstructured":"Howard Dale David Jennings and Terry Rudolph. 2015. Provable quantum advantage in randomness processing. Nature communications 6(2015) 8203. https:\/\/doi.org\/10.1038\/ncomms9203","DOI":"10.1038\/ncomms9203"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_2_1_16_1","volume-title":"Quantum walks on a programmable two-dimensional 62-qubit superconducting processor. Science 372, 6545","author":"Gong Ming","year":"2021","unstructured":"Ming Gong , Shiyu Wang , Chen Zha , Ming-Cheng Chen , He-Liang Huang , Yulin Wu , Qingling Zhu , Youwei Zhao , Shaowei Li , Shaojun Guo , 2021. Quantum walks on a programmable two-dimensional 62-qubit superconducting processor. Science 372, 6545 ( 2021 ), 948\u2013952. https:\/\/doi.org\/10.1126\/science.abg7812 10.1126\/science.abg7812 Ming Gong, Shiyu Wang, Chen Zha, Ming-Cheng Chen, He-Liang Huang, Yulin Wu, Qingling Zhu, Youwei Zhao, Shaowei Li, Shaojun Guo, 2021. Quantum walks on a programmable two-dimensional 62-qubit superconducting processor. Science 372, 6545 (2021), 948\u2013952. https:\/\/doi.org\/10.1126\/science.abg7812"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000192"},{"key":"#cr-split#-e_1_3_2_1_18_1.1","unstructured":"Martin Hofmann and Georg Moser. 2015. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a038). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik 241-256. https:\/\/doi.org\/10.4230\/LIPIcs.TLCA.2015.241 10.4230\/LIPIcs.TLCA.2015.241"},{"key":"#cr-split#-e_1_3_2_1_18_1.2","unstructured":"Martin Hofmann and Georg Moser. 2015. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)(Leibniz International Proceedings in Informatics (LIPIcs) Vol.\u00a038). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik 241-256. https:\/\/doi.org\/10.4230\/LIPIcs.TLCA.2015.241"},{"key":"e_1_3_2_1_19_1","volume-title":"Matrix analysis","author":"Horn A","unstructured":"Roger\u00a0 A Horn and Charles\u00a0 R Johnson . 2012. Matrix analysis . Cambridge university press . Roger\u00a0A Horn and Charles\u00a0R Johnson. 2012. Matrix analysis. Cambridge university press."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.parco.2014.12.001"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11128-018-2017-4"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Junyi Liu Li Zhou Gilles Barthe and Mingsheng Ying. 2022. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs (Extended Version). arXiv preprint arXiv:1911.12557(2022).  Junyi Liu Li Zhou Gilles Barthe and Mingsheng Ying. 2022. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs (Extended Version). arXiv preprint arXiv:1911.12557(2022).","DOI":"10.1145\/3531130.3533327"},{"key":"e_1_3_2_1_25_1","volume-title":"refinement and proof for probabilistic systems","author":"McIver Annabelle","unstructured":"Annabelle McIver , Carroll Morgan , and Charles\u00a0Carroll Morgan . 2005. Abstraction , refinement and proof for probabilistic systems . Springer Science & Business Media . Annabelle McIver, Carroll Morgan, and Charles\u00a0Carroll Morgan. 2005. Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media."},{"key":"e_1_3_2_1_26_1","volume-title":"ACM SIGPLAN Notices, Vol.\u00a053. ACM","author":"Ngo Van\u00a0Chan","year":"1923","unstructured":"Van\u00a0Chan Ngo , Quentin Carbonneaux , and Jan Hoffmann . 2018. Bounded expectations: resource analysis for probabilistic programs . In ACM SIGPLAN Notices, Vol.\u00a053. ACM , Association for Computing Machinery , 496\u2013512. https:\/\/doi.org\/10.1145\/3296979.3 1923 94 10.1145\/3296979.3192394 Van\u00a0Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. 2018. Bounded expectations: resource analysis for probabilistic programs. In ACM SIGPLAN Notices, Vol.\u00a053. ACM, Association for Computing Machinery, 496\u2013512. https:\/\/doi.org\/10.1145\/3296979.3192394"},{"key":"e_1_3_2_1_27_1","volume-title":"Verifying and Synthesizing Constant-Resource Implementations with Types. In 2017 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, 710\u2013728","author":"Ngo Van\u00a0Chan","year":"2017","unstructured":"Van\u00a0Chan Ngo , Mario Dehesa-Azuara , Matthew Fredrikson , and Jan Hoffmann . 2017 . Verifying and Synthesizing Constant-Resource Implementations with Types. In 2017 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, 710\u2013728 . https:\/\/doi.org\/10.1109\/SP.2017.53 10.1109\/SP.2017.53 Van\u00a0Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, and Jan Hoffmann. 2017. Verifying and Synthesizing Constant-Resource Implementations with Types. In 2017 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, 710\u2013728. https:\/\/doi.org\/10.1109\/SP.2017.53"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Michael\u00a0A Nielsen and Isaac Chuang. 2002. Quantum computation and quantum information.  Michael\u00a0A Nielsen and Isaac Chuang. 2002. Quantum computation and quantum information.","DOI":"10.1119\/1.1463744"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90029-3"},{"key":"e_1_3_2_1_30_1","unstructured":"Federico Olmedo and Alejandro D\u00edaz-Caro. 2019. Runtime Analysis of Quantum Programs: A Formal Approach. arXiv preprint arXiv:1911.11247(2019).  Federico Olmedo and Alejandro D\u00edaz-Caro. 2019. Runtime Analysis of Quantum Programs: A Formal Approach. arXiv preprint arXiv:1911.11247(2019)."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-08-06-79"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70697-9_9"},{"key":"e_1_3_2_1_34_1","volume-title":"Quantum Programming. In Proceedings of the 5th International Conference on Mathematics of Program Construction (MPC 2000)","author":"Sanders J.","year":"1837","unstructured":"J. Sanders and P. Zuliani . 2000 . Quantum Programming. In Proceedings of the 5th International Conference on Mathematics of Program Construction (MPC 2000) (LNCS, Vol.\u00a0 1837 ). Springer Berlin Heidelberg, 80\u201399. https:\/\/doi.org\/10.1007\/10722010_6 10.1007\/10722010_6 J. Sanders and P. Zuliani. 2000. Quantum Programming. In Proceedings of the 5th International Conference on Mathematics of Program Construction (MPC 2000)(LNCS, Vol.\u00a01837). Springer Berlin Heidelberg, 80\u201399. https:\/\/doi.org\/10.1007\/10722010_6"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.67.052307"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_32"},{"key":"e_1_3_2_1_38_1","article-title":"Floyd\u2013Hoare Logic for Quantum Programs","volume":"33","author":"Ying Mingsheng","year":"2012","unstructured":"Mingsheng Ying . 2012 . Floyd\u2013Hoare Logic for Quantum Programs . ACM Trans. Program. Lang. Syst. 33 , 6, Article 19(2012). https:\/\/doi.org\/10.1145\/2049706.2049708 10.1145\/2049706.2049708 Mingsheng Ying. 2012. Floyd\u2013Hoare Logic for Quantum Programs. ACM Trans. Program. Lang. Syst. 33, 6, Article 19(2012). https:\/\/doi.org\/10.1145\/2049706.2049708","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan Kaufmann.  Mingsheng Ying. 2016. Foundations of Quantum Programming. Morgan Kaufmann.","DOI":"10.1016\/B978-0-12-802306-8.00005-7"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.016"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"}],"event":{"name":"LICS '22: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Haifa Israel","acronym":"LICS '22","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533327","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3531130.3533327","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:09Z","timestamp":1750186929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3531130.3533327"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,2]]},"references-count":43,"alternative-id":["10.1145\/3531130.3533327","10.1145\/3531130"],"URL":"https:\/\/doi.org\/10.1145\/3531130.3533327","relation":{},"subject":[],"published":{"date-parts":[[2022,8,2]]},"assertion":[{"value":"2022-08-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}