{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:40Z","timestamp":1780994620520,"version":"3.54.1"},"reference-count":86,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"the National Key R&D Program of China","award":["No. 2023YFA1009403"],"award-info":[{"award-number":["No. 2023YFA1009403"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            We define QSE, a symbolic execution framework for quantum programs by integrating symbolic variables into quantum states and the outcomes of quantum measurements. The soundness of QSE is established through a theorem that ensures the correctness of symbolic execution within operational semantics. We further introduce symbolic stabilizer states, which symbolize the phases of stabilizer generators, for the efficient analysis of quantum error correction (QEC) programs. Within the QSE framework, we can use symbolic expressions to characterize the possible discrete Pauli errors in QEC, providing a significant improvement over existing methods that rely on sampling with simulators. We implement QSE with the support of symbolic stabilizer states in a prototype tool named\n            <jats:monospace>QuantumSE.jl<\/jats:monospace>\n            . Our experiments on representative QEC codes, including quantum repetition codes, Kitaev\u2019s toric codes, and quantum Tanner codes, demonstrate the efficiency of\n            <jats:monospace>QuantumSE.jl<\/jats:monospace>\n            for debugging QEC programs with over 1000 qubits. In addition, by substituting concrete values in symbolic expressions of measurement results,\n            <jats:monospace>QuantumSE.jl<\/jats:monospace>\n            is also equipped with a sampling feature for stabilizer circuits. Despite a longer initialization time than the state-of-the-art stabilizer simulator, Google\u2019s Stim, QuantumSE.jl offers a quicker sampling rate in the experiments.\n          <\/jats:p>","DOI":"10.1145\/3656419","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1040-1065","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Symbolic Execution for Quantum Error Correction Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7628-1185","authenticated-orcid":false,"given":"Wang","family":"Fang","sequence":"first","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, China"},{"name":"University of Chinese Academy of Sciences, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4847-702X","authenticated-orcid":false,"given":"Mingsheng","family":"Ying","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, Beijing, China"},{"name":"Tsinghua University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.70.052328"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-022-04819-6"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-022-05434-1"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/258533.258579"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046745"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.73.022334"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-019-1666-5"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SAT.2022.18"},{"key":"e_1_3_1_11_1","unstructured":"Ville Bergholm Josh Izaac Maria Schuld Christian Gogolin Shahnawaz Ahmed Vishnu Ajith M Sohaib Alam Guillermo Alonso-Linaje B AkashNarayanan et al. 2022. PennyLane: Automatic differentiation of hybrid quantum-classical computations. arXiv:1811.04968 [quant-ph]"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1137\/141000671"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-023-06927-3"},{"key":"e_1_3_1_14_1","unstructured":"Lukas Burgholzer Alexander Ploier and Robert Wille. 2023. Tensor Networks or Decision Diagrams? Guidelines for Classical Quantum Circuit Simulation. arXiv:2302.06616 [quant-ph]"},{"key":"e_1_3_1_15_1","first-page":"209","volume-title":"8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008. USENIX Association, 209\u2013224. http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571786.3573018"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591270"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-021-03588-y"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Cirq Developers. 2018. Cirq. https:\/\/doi.org\/10.5281\/zenodo.4062499 10.5281\/zenodo.4062499","DOI":"10.5281\/zenodo.4062499"},{"key":"e_1_3_1_22_1","unstructured":"Hubert Comon Max Dauchet R\u00e9mi Gilleron Florent Jacquemard Denis Lugiez Christof L\u00f6ding Sophie Tison and Marc Tommasi. 2008. Tree Automata Techniques and Applications. 262 pages. https:\/\/inria.hal.science\/hal-03367725"},{"key":"e_1_3_1_23_1","unstructured":"Andrew W. Cross Lev S. Bishop John A. Smolin and Jay M. Gambetta. 2017. Open Quantum Assembly Language. arXiv:1707.03429 [quant-ph]"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.1499754"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.4153\/CJM-1965-045-4"},{"key":"e_1_3_1_27_1","doi-asserted-by":"crossref","unstructured":"Wang Fang and Mingsheng Ying. 2023. Symbolic Execution for Quantum Error Correction Programs (Extended Version). arXiv:2311.11313 [quant-ph]","DOI":"10.1145\/3656419"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Wang Fang and Mingsheng Ying. 2024. Artifact: Symbolic Execution for Quantum Error Correction Programs. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.10781381 10.5281\/zenodo.10781381","DOI":"10.5281\/zenodo.10781381"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354175"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.86.032324"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2021-07-06-497"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_1_34_1","volume-title":"Ph. D. Dissertation","author":"Gottesman Daniel","year":"1997","unstructured":"Daniel Gottesman. 1997. Stabilizer codes and quantum error correction. Ph. D. Dissertation. California Institute of Technology. arXiv:quant-ph\/9705052 [quant-ph]"},{"key":"e_1_3_1_35_1","unstructured":"Daniel Gottesman. 1998. The Heisenberg Representation of Quantum Computers. arXiv:quant-ph\/9807006 [quant-ph]"},{"key":"e_1_3_1_36_1","doi-asserted-by":"crossref","unstructured":"Daniel Gottesman. 2014. Fault-Tolerant Quantum Computation with Constant Overhead. arXiv:1310.2984 [quant-ph]","DOI":"10.26421\/QIC14.15-16-5"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2021.21"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3514355"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446750"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3307650.3322213"},{"key":"e_1_3_1_42_1","unstructured":"IBM. 2023. The hardware and software for the era of quantum utility is here. https:\/\/www.ibm.com\/quantum\/blog\/quantum-roadmap-2033."},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0003-4916(02)00018-0"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5923-8_19"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12532-009-0002-8"},{"key":"e_1_3_1_47_1","unstructured":"Stefan Krastanov. 2019. https:\/\/quantumsavory.github.io\/QuantumClifford.jl\/stable\/ Accessed on 2023-7-7."},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","unstructured":"Anthony Leverrier and Gilles Z\u00e9mor. 2022. Quantum Tanner codes. In 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS). 872\u2013883. https:\/\/doi.org\/10.1109\/FOCS54457.2022.00117 10.1109\/FOCS54457.2022.00117","DOI":"10.1109\/FOCS54457.2022.00117"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428218"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378488"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2643011"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2020-10-11-341"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-022-04725-x"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1137\/050644756"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2459034"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1038\/s42254-019-0086-7"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.128.030501"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519935.3520017"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009894"},{"key":"e_1_3_1_62_1","first-page":"181","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Poeplau Sebastian","year":"2020","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with SymCC: Don\u2019t interpret, compile!. In 29th USENIX Security Symposium (USENIX Security 20). USENIX Association, 181\u2013198. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/poeplau"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","unstructured":"Qiskit Community. 2017. Qiskit: An Open-Source Framework for Quantum Computing. https:\/\/doi.org\/10.5281\/zenodo.2562110 10.5281\/zenodo.2562110","DOI":"10.5281\/zenodo.2562110"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.99.062337"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.266.8"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.340.14"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3566097.3567929"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","unstructured":"P. W. Shor. 1996. Fault-tolerant quantum computation. In Proceedings of 37th Conference on Foundations of Computer Science (Proceedings of 37th Conference on Foundations of Computer Science). 56\u201365. https:\/\/doi.org\/10.1109\/SFCS.1996.548464 10.1109\/SFCS.1996.548464","DOI":"10.1109\/SFCS.1996.548464"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1348250.1348256"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","unstructured":"Meghana Aparna Sistla Swarat Chaudhuri and Thomas Reps. 2024. CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams. ACM Trans. Program. Lang. Syst. (mar 2024). https:\/\/doi.org\/10.1145\/3651157 10.1145\/3651157 Just Accepted.","DOI":"10.1145\/3651157"},{"key":"e_1_3_1_72_1","unstructured":"Aarthi Sundaram Robert Rand Kartik Singhal and Brad Lackey. 2022. Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs. https:\/\/ks.cs.uchicago.edu\/publication\/heisenberg\/"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563344"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2021-10-06-559"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183895.3183901"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","unstructured":"Yuan-Hung Tsai Jie-Hong R. Jiang and Chiao-Shan Jhang. 2021. Bit-Slicing the Hilbert Space: Scaling Up Accurate Quantum Circuit Simulation. In 2021 58th ACM\/IEEE Design Automation Conference (DAC). 439\u2013444. https:\/\/doi.org\/10.1109\/DAC18074.2021.9586191 10.1109\/DAC18074.2021.9586191","DOI":"10.1109\/DAC18074.2021.9586191"},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2023-09-11-1108"},{"key":"e_1_3_1_79_1","unstructured":"Anbang Wu Gushu Li Hezi Zhang Gian Giacomo Guerreschi Yuan Xie and Yufei Ding. 2021b. QECV: Quantum Error Correction Verification. arXiv:2111.13728 [quant-ph]"},{"key":"e_1_3_1_80_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.127.180501"},{"key":"e_1_3_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523433"},{"key":"e_1_3_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_1_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.94"},{"key":"e_1_3_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380419"},{"key":"e_1_3_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_1_86_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.129.030501"},{"key":"e_1_3_1_87_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\/3656419","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656419","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:41:33Z","timestamp":1751661693000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656419"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":86,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656419"],"URL":"https:\/\/doi.org\/10.1145\/3656419","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}