{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T11:08:54Z","timestamp":1790075334857,"version":"4.0.1"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["OMA-2016245"],"award-info":[{"award-number":["OMA-2016245"]}],"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":["HR00112520301"],"award-info":[{"award-number":["HR00112520301"]}],"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":[[2026,6,8]]},"abstract":"<jats:p>\n                    Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Existing verification techniques are insufficient\u2014even for quantum circuits, a deliberately restricted model that lacks classical control, but still underpins many current quantum algorithms. Many existing formal methods require exponential time and space to represent and manipulate (representations of) assertions and judgments, making them impractical for quantum circuits with many qubits. This paper presents SAQR-QC, a logic for\n                    <jats:bold>S<\/jats:bold>\n                    calable but\n                    <jats:bold>A<\/jats:bold>\n                    pproximate\n                    <jats:bold>Q<\/jats:bold>\n                    uantitative\n                    <jats:bold>R<\/jats:bold>\n                    easoning about\n                    <jats:bold>Q<\/jats:bold>\n                    uantum\n                    <jats:bold>C<\/jats:bold>\n                    ircuits. SAQR-QC has three characteristics: (i) some deliberate loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) every reasoning step is local\u2014involving just a small number of qubits\u2014making reasoning scalable. We demonstrate the effectiveness of SAQR-QC via two case studies: the verification of GHZ circuits involving non-Clifford gates, and the analysis of quantum phase estimation\u2014a core subroutine in Shor\u2019s factoring algorithm.\n                  <\/jats:p>","DOI":"10.1145\/3808284","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"928-952","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits"],"prefix":"10.1145","volume":"10","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\/0000-0003-4747-365X","authenticated-orcid":false,"given":"Jens","family":"Palsberg","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, Los Angeles, 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, Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"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.1145\/3725725"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3776712"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_28"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704873"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.1113479"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.22331\/q-2023-11-20-1185"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.2307\/1968621"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.003"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591270"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39910-0_11"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_1_18_2","unstructured":"Crab. 2023. Crab: A C++ Library for Building Program Static Analyses. https:\/\/github.com\/seahorn\/crab#tab=readme-ov-file. GitHub repository accessed: 2023-10-26."},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_38"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-95561-8_8"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.103.150502"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3604630"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10622-4_7"},{"key":"e_1_3_1_27_2","unstructured":"A. Yu. Kitaev. 1995. Quantum measurements and the Abelian Stabilizer Problem. arXiv:quant-ph\/9511026 (1995) 22 pages."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498697"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3807780"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/347324.348031"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2021.136"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.5555\/1972505"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.2218775120"},{"key":"e_1_3_1_35_2","unstructured":"Robert Rand. 2019. Verification logics for quantum programs. arXiv preprint arXiv:1904.04304 (2019) 42 pages."},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1088\/1751-8113\/46\/5\/055304"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250750"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795293172"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454029"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2049078"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.87.052310"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470673"},{"key":"e_1_3_1_51_2","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\/pdf\/10.1145\/3808284","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808284","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:50:53Z","timestamp":1790074253000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808284"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":50,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808284"],"URL":"https:\/\/doi.org\/10.1145\/3808284","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-12","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}