{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T05:11:08Z","timestamp":1780463468456,"version":"3.54.1"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100013290","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2018YFA0306701"],"award-info":[{"award-number":["2018YFA0306701"]}],"id":[{"id":"10.13039\/501100013290","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science Foundation","award":["1730309, 1925717"],"award-info":[{"award-number":["1730309, 1925717"]}]},{"DOI":"10.13039\/501100012659","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61832015"],"award-info":[{"award-number":["61832015"]}],"id":[{"id":"10.13039\/501100012659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"crossref","award":["DE180100156, DP160101652, DP180100691"],"award-info":[{"award-number":["DE180100156, DP160101652, DP180100691"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following Birkhoff-von Neumann quantum logic. The satisfaction of a projection by a quantum state can be directly checked upon a small number of projective measurements rather than a large number of repeated executions. On the theory side, we rigorously prove that checking projection-based assertions can help locate bugs or statistically assure that the semantic function of the tested program is close to what we expect, for both exact and approximate quantum programs. On the practice side, we consider hardware constraints and introduce several techniques to transform the assertions, making them directly executable on the measurement-restricted quantum computers. We also propose to achieve simplified assertion implementation using local projection technique with soundness guaranteed. We compare Proq with existing quantum program assertions and demonstrate the effectiveness and efficiency of Proq by its applications to assert two sophisticated quantum algorithms, the Harrow-Hassidim-Lloyd algorithm and Shor\u2019s algorithm.<\/jats:p>","DOI":"10.1145\/3428218","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:40:14Z","timestamp":1606261214000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":93,"title":["Projection-based runtime assertions for testing and debugging Quantum programs"],"prefix":"10.1145","volume":"4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6233-0334","authenticated-orcid":false,"given":"Gushu","family":"Li","sequence":"first","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Li","family":"Zhou","sequence":"additional","affiliation":[{"name":"MPI-SP, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nengkun","family":"Yu","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yufei","family":"Ding","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"University of Technology Sydney, Australia \/ Institute of Software at Chinese Academy of Sciences, China \/ Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuan","family":"Xie","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, Fred Chong, Margaret Martonosi, Martin Suchara, Ken Brown, Massoud Pedram, and Todd Brun. [n.d.].","author":"Abhari Ali Javadi","year":"2012"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"Garrett Birkhof and John Von Neumann. 1936. The logic of quantum mechanics. Annals of mathematics ( 1936 ) 823\u015b843.  Garrett Birkhof and John Von Neumann. 1936. The logic of quantum mechanics. Annals of mathematics ( 1936 ) 823\u015b843.","DOI":"10.2307\/1968621"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"Vladimir B Braginsky Yuri I Vorontsov and Kip S Thorne. 1980. Quantum nondemolition measurements. Science 209 4456 ( 1980 ) 547\u015b557.  Vladimir B Braginsky Yuri I Vorontsov and Kip S Thorne. 1980. Quantum nondemolition measurements. Science 209 4456 ( 1980 ) 547\u015b557.","DOI":"10.1126\/science.209.4456.547"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749904000067"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.86.022339"},{"key":"e_1_2_2_6_1","volume-title":"Classical simulation of intermediate-size quantum circuits. arXiv preprint arXiv","author":"Chen Jianxin","year":"1805"},{"key":"e_1_2_2_7_1","unstructured":"Google. 2018. Announcing Cirq : An Open Source Framework for NISQ Algorithms. https:\/\/ai.googleblog.com\/ 2018 \/07\/ announcing-cirq-open-source-framework. html.  Google. 2018. Announcing Cirq : An Open Source Framework for NISQ Algorithms. https:\/\/ai.googleblog.com\/ 2018 \/07\/ announcing-cirq-open-source-framework. html."},{"key":"e_1_2_2_8_1","volume-title":"Neil J Ross, Peter Selinger, and Beno\u00eet Valiron.","author":"Green Alexander S","year":"2013"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Aram W Harrow Avinatan Hassidim and Seth Lloyd. 2009. Quantum algorithm for linear systems of equations. Physical review letters 103 15 ( 2009 ) 150502.  Aram W Harrow Avinatan Hassidim and Seth Lloyd. 2009. Quantum algorithm for linear systems of equations. Physical review letters 103 15 ( 2009 ) 150502.","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_2_2_11_1","volume-title":"A Verified Optimizer for Quantum Circuits. arXiv preprint arXiv","author":"Hietala Kesha","year":"1912"},{"key":"e_1_2_2_12_1","unstructured":"Yipeng Huang and Margaret Martonosi. 2019a. QDB: From Quantum Algorithms Towards Correct Quantum Programs. In 9th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU 2018 ). Schloss DagstuhlLeibniz-Zentrum fuer Informatik.  Yipeng Huang and Margaret Martonosi. 2019a. QDB: From Quantum Algorithms Towards Correct Quantum Programs. In 9th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU 2018 ). Schloss DagstuhlLeibniz-Zentrum fuer Informatik."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3307650.3322213"},{"key":"e_1_2_2_14_1","unstructured":"IBM. 2019. Gate and operation specification for quantum circuits. https:\/\/github.com\/Qiskit\/openqasm.  IBM. 2019. Gate and operation specification for quantum circuits. https:\/\/github.com\/Qiskit\/openqasm."},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Ali JavadiAbhari Shruti Patil Daniel Kudrow Jef Heckey Alexey Lvov Frederic T Chong and Margaret Martonosi. 2015. ScafCC: Scalable compilation and analysis of quantum programs. Parallel Comput. 45 ( 2015 ) 2\u015b17.  Ali JavadiAbhari Shruti Patil Daniel Kudrow Jef Heckey Alexey Lvov Frederic T Chong and Margaret Martonosi. 2015. ScafCC: Scalable compilation and analysis of quantum programs. Parallel Comput. 45 ( 2015 ) 2\u015b17.","DOI":"10.1016\/j.parco.2014.12.001"},{"key":"e_1_2_2_16_1","volume-title":"Orthomodular lattices","author":"Kalmbach Gudrun"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.89.042338"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.89.207901"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378488"},{"key":"e_1_2_2_20_1","doi-asserted-by":"crossref","unstructured":"Seth Lloyd Masoud Mohseni and Patrick Rebentrost. 2014. Quantum principal component analysis. Nature Physics 10 9 ( 2014 ) 631\u015b633.  Seth Lloyd Masoud Mohseni and Patrick Rebentrost. 2014. Quantum principal component analysis. Nature Physics 10 9 ( 2014 ) 631\u015b633.","DOI":"10.1038\/nphys3029"},{"key":"e_1_2_2_21_1","volume-title":"Isaac L. Chuang","author":"Nielsen Michael A","year":"2010"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Alberto Peruzzo Jarrod McClean Peter Shadbolt Man-Hong Yung Xiao-Qi Zhou Peter J Love Al\u00e1n Aspuru-Guzik and Jeremy L O'brien. 2014. A variational eigenvalue solver on a photonic quantum processor. Nature communications 5 ( 2014 ) 4213.  Alberto Peruzzo Jarrod McClean Peter Shadbolt Man-Hong Yung Xiao-Qi Zhou Peter J Love Al\u00e1n Aspuru-Guzik and Jeremy L O'brien. 2014. A variational eigenvalue solver on a photonic quantum processor. Nature communications 5 ( 2014 ) 4213.","DOI":"10.1038\/ncomms5213"},{"key":"e_1_2_2_24_1","volume-title":"QWIRE practice: Formal verification of quantum circuits in Coq. arXiv preprint arXiv","author":"Rand Robert","year":"1803"},{"key":"e_1_2_2_25_1","unstructured":"Rigetti. 2019. A Python library for quantum programming using Quil. https:\/\/github.com\/rigetti\/pyquil.  Rigetti. 2019. A Python library for quantum programming using Quil. https:\/\/github.com\/rigetti\/pyquil."},{"key":"e_1_2_2_26_1","unstructured":"Rigetti Forest team. 2019. Forest SDK. https:\/\/www.rigetti.com\/forest.  Rigetti Forest team. 2019. Forest SDK. https:\/\/www.rigetti.com\/forest."},{"key":"e_1_2_2_27_1","volume-title":"Contract-based verification of a realistic quantum compiler. arXiv preprint arXiv","author":"Shi Yunong","year":"1908"},{"key":"e_1_2_2_28_1","series-title":"SIAM review 41, 2 ( 1999 ), 303\u015b332","volume-title":"Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer","author":"Shor Peter W"},{"key":"e_1_2_2_29_1","volume-title":"Enabling scalable quantum computing and development with a high-level domain-specific language. arXiv preprint arXiv","author":"Svore Krysta M","year":"1803"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"Lieven MK Vandersypen Matthias Stefen Gregory Breyta Costantino S Yannoni Mark H Sherwood and Isaac L Chuang. 2001. Experimental realization of Shor's quantum factoring algorithm using nuclear magnetic resonance. Nature 414 6866 ( 2001 ) 883.  Lieven MK Vandersypen Matthias Stefen Gregory Breyta Costantino S Yannoni Mark H Sherwood and Isaac L Chuang. 2001. Experimental realization of Shor's quantum factoring algorithm using nuclear magnetic resonance. Nature 414 6866 ( 2001 ) 883.","DOI":"10.1038\/414883a"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/18.796385"},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","unstructured":"William K Wootters and Wojciech H Zurek. 1982. A single quantum cannot be cloned. Nature 299 5886 ( 1982 ) 802.  William K Wootters and Wojciech H Zurek. 1982. A single quantum cannot be cloned. Nature 299 5886 ( 1982 ) 802.","DOI":"10.1038\/299802a0"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.118.020401"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_2_36_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_2_2_37_1","doi-asserted-by":"crossref","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\u015b360.  Mingsheng Ying Runyao Duan Yuan Feng and Zhengfeng Ji. 2010. Predicate transformer semantics of quantum programs. Semantic Techniques in Quantum Computation 8 ( 2010 ) 311\u015b360.","DOI":"10.1017\/CBO9781139193313.009"},{"key":"e_1_2_2_38_1","volume-title":"Quantum Temporal Logic. arXiv","author":"Nengkun Yu.","year":"1908"},{"key":"e_1_2_2_39_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\/3428218","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428218","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428218","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428218"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":39,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428218"],"URL":"https:\/\/doi.org\/10.1145\/3428218","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}