{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:11:57Z","timestamp":1784200317343,"version":"3.55.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2212558"],"award-info":[{"award-number":["CCF-2212558"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011252030"],"award-info":[{"award-number":["HR0011252030"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    This paper concerns the problem of checking if two shallow (i.e., constant-depth) quantum circuits perform equivalent computations. Equivalence checking is a fundamental correctness question\u2014needed, e.g., for ensuring that transformations applied to a quantum circuit do not alter its behavior. For quantum circuits, the problem is challenging because a straightforward representation on a classical computer of each circuit\u2019s quantum state can require time and space that are exponential in the number of qubits\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    .\n                  <\/jats:p>\n                  <jats:p>\n                    The paper presents\n                    <jats:italic toggle=\"yes\">Projection-Based Equivalence Checking<\/jats:italic>\n                    (PBEC), which provides decision procedures for two variants of the equivalence-checking problem. Both can be carried out on a classical computer in time and space that, for any fixed depth, is linear in\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    . Our key insight is that local projections can serve as constraints that fully characterize the output state of a shallow quantum circuit. The output state is the unique quantum state that satisfies all the constraints. Beyond equivalence checking, we show how to use the constraint representation to check a class of assertions, both statically and at run time. Our assertion-checking methods are sound and complete for assertions expressed as conjunctions of local projections.\n                  <\/jats:p>\n                  <jats:p>\n                    Our experiments showed that computing the constraint representation of a random 100-qubit 1D circuit of depth 6 takes 129.64 seconds. Equivalence checking between two random 100-qubit 1D circuits of depth 3 requires 4.46 seconds for fixed input\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mo stretchy=\"false\">|<\/mml:mo>\n                          <mml:mn>0<\/mml:mn>\n                          <mml:msup>\n                            <mml:mtext>\u232a<\/mml:mtext>\n                            <mml:mrow>\n                              <mml:mo>\u2297<\/mml:mo>\n                              <mml:mn>100<\/mml:mn>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    , and no more than 31.96 seconds for arbitrary inputs. Computing the constraint description for a random 100-qubit circuit of depth 3 takes 6.99 seconds for a 2D structure, compared to 10.67 seconds for a circuit with arbitrary connectivity. At depth 2, equivalence checking takes 0.20 seconds for fixed input and 0.44 seconds for arbitrary input, with similar performance for both 2D and arbitrary-connectivity circuits.\n                  <\/jats:p>","DOI":"10.1145\/3763153","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"2870-2897","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Scalable Equivalence Checking and Verification of Shallow Quantum Circuits"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1188-3032","authenticated-orcid":false,"given":"Nengkun","family":"Yu","sequence":"first","affiliation":[{"name":"Stony Brook University, Stony Brook, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-5610-462X","authenticated-orcid":false,"given":"Xuan Du","family":"Trinh","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1103\/physreva.70.052328"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.287.1"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-019-1666-5"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90001-9"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167093"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2023-11-20-1185"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.2307\/1968621"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.aar3106"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41567-020-0948-z"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3618260.3649638"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.simpa.2020.100051"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0024-3795(75)90075-0"},{"key":"e_1_3_1_15_2","unstructured":"Fred Chong. 2018. Verifying Quantum Software and Hardware. https:\/\/www.sigarch.org\/verifying-quantum-software-and-hardware\/. [Online; accessed Jun 18 2018]."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09526-8_20"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.1985.0070"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539792228228"},{"key":"e_1_3_1_19_2","unstructured":"Daniel Gottesman. 1998. The Heisenberg Representation of Quantum Computers. arXiv:quant-ph\/9807006 [quant-ph] https:\/\/arxiv.org\/abs\/quant-ph\/9807006"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3508352.3549479"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290344"},{"key":"e_1_3_1_23_2","unstructured":"Zhengfeng Ji and Xiaodi Wu. 2009. Non-Identity Check Remains QMA-Complete for Short Circuits. arXiv:0906.5416 [quant-ph] https:\/\/arxiv.org\/abs\/0906.5416"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498697"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428218"},{"key":"e_1_3_1_26_2","first-page":"136:1","volume-title":"Proceedings of the 48th International Colloquium on Automata, Languages, and Programming","author":"Li Yangjia","year":"2021","unstructured":"Yangjia Li and Dominique Unruh. 2021. Quantum Relational Hoare Logic with Expectations. In Proceedings of the 48th International Colloquium on Automata, Languages, and Programming. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 136:1\u2013136:20."},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-63501-4_21"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-024-07998-6"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevX.12.021021"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.5555\/1972505"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.2218775120"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-08-06-79"},{"key":"e_1_3_1_33_2","unstructured":"Thomas Schuster Jonas Haferkamp and Hsin-Yuan Huang. 2025. Random unitaries in extremely low depth. arXiv:2407.07754 [quant-ph] https:\/\/arxiv.org\/abs\/2407.07754"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3651157"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454029"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_3_1_37_2","doi-asserted-by":"crossref","unstructured":"Barbara M. Terhal and David P. DiVincenzo. 2004. Adaptive Quantum Computation Constant Depth Quantum Circuits and Arthur-Merlin Games. arXiv:quant-ph\/0205133 [quant-ph] https:\/\/arxiv.org\/abs\/quant-ph\/0205133","DOI":"10.26421\/QIC4.2-5"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-45332-8_10"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_3_1_40_2","volume-title":"Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019)","author":"Dominique Unruh","year":"2019","unstructured":"Dominique Unruh. 2019. Quantum relational Hoare logic. In Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). ACM, New York, NY, USA."},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397246"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.22331\/Q-2023-09-11-1108"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523433"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/2011464.2011465"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527316"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65633-0_22"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_1_49_2","unstructured":"Nengkun Yu Xuan Du Trinh and Thomas Reps. 2025. Scalable Equivalence Checking and Verification of Shallow Quantum Circuits. arXiv:2504.01558 [quant-ph] https:\/\/arxiv.org\/abs\/2504.01558"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.91.032302"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656397"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498691"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2834427"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10710-021-09407-7"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763153","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763153","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:16:47Z","timestamp":1784197007000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":54,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763153"],"URL":"https:\/\/doi.org\/10.1145\/3763153","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}