{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,3]],"date-time":"2026-02-03T18:25:32Z","timestamp":1770143132044,"version":"3.49.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ARC Discovery Program","award":["#DP210102449"],"award-info":[{"award-number":["#DP210102449"]}]},{"name":"ARC DECRA","award":["#DE180100156"],"award-info":[{"award-number":["#DE180100156"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,4,29]]},"abstract":"<jats:p>Bug-catching is important for developing quantum programs. Motivated by the incorrectness logic for classical programs, we propose an incorrectness logic towards a logical foundation for static bug-catching in quantum programming. The validity of formulas in this logic is dual to that of quantum Hoare logics. We justify the formulation of validity by an intuitive explanation from a reachability point of view and a comparison against several alternative formulations. Compared with existing works focusing on dynamic analysis, our logic provides sound and complete arguments. We further demonstrate the usefulness of the logic by reasoning several examples, including Grover's search, quantum teleportation, and a repeat-until-success program. We also automate the reasoning procedure by a prototyped static analyzer built on top of the logic rules.<\/jats:p>","DOI":"10.1145\/3527316","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["On incorrectness logic for Quantum programs"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2930-7447","authenticated-orcid":false,"given":"Peng","family":"Yan","sequence":"first","affiliation":[{"name":"University of Technology Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5965-1209","authenticated-orcid":false,"given":"Hanru","family":"Jiang","sequence":"additional","affiliation":[{"name":"BIMSA, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1188-3032","authenticated-orcid":false,"given":"Nengkun","family":"Yu","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Scaffold: Quantum programming language.","author":"Abhari Ali J","year":"2012","unstructured":"Ali J Abhari , Arvin Faruque , Mohammad J Dousti , Lukas Svec , Oana Catu , Amlan Chakrabati , Chen-Fu Chiang , Seth Vanderwilt , John Black , and Fred Chong . 2012 . Scaffold: Quantum programming language. Princeton Univ NJ Dept of Computer Science . Ali J Abhari, Arvin Faruque, Mohammad J Dousti, Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, and Fred Chong. 2012. Scaffold: Quantum programming language. Princeton Univ NJ Dept of Computer Science."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.2562111"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-019-1666-5"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968621"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276514"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.114.080502"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3505636"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5182845"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290370"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462177"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.PLATEAU.2018.4"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3307650.3322213"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290344"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.parco.2014.12.001"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428218"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.89.042338"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378488"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.26421\/QIC14.15-16-2"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009894"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.028"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.266.8"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004256"},{"key":"e_1_2_1_31_1","volume-title":"Zeng","author":"Smith Robert S.","year":"2016","unstructured":"Robert S. Smith , Michael J. Curtis , and William J . Zeng . 2016 . A Practical Quantum Instruction Set Architecture . arxiv:1608.03355. Robert S. Smith, Michael J. Curtis, and William J. Zeng. 2016. A Practical Quantum Instruction Set Architecture. arxiv:1608.03355."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454029"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Peng Yan Hanru Jiang and Nengkun Yu. 2022. On Incorrectness Logic for Quantum Programs (Technical Report). https:\/\/hrjiang.github.io\/ilq\/  Peng Yan Hanru Jiang and Nengkun Yu. 2022. On Incorrectness Logic for Quantum Programs (Technical Report). https:\/\/hrjiang.github.io\/ilq\/","DOI":"10.1145\/3527316"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/C2014-0-02660-3"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139193313.009"},{"key":"e_1_2_1_39_1","unstructured":"Nengkun Yu. 2019. Quantum Temporal Logic. https:\/\/doi.org\/10.48550\/arXiv.1908.00158  Nengkun Yu. 2019. Quantum Temporal Logic. https:\/\/doi.org\/10.48550\/arXiv.1908.00158"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_7"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.abe8770"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527316","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527316","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:52Z","timestamp":1750191532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527316"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":44,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527316"],"URL":"https:\/\/doi.org\/10.1145\/3527316","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}