{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:10:53Z","timestamp":1746115853919,"version":"3.40.4"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906596"},{"type":"electronic","value":"9783031906602"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Equivalence checking plays a crucial role in quantum circuit compilation, optimization, and verification. Stabilizer circuits can be simulated classically by tracking the so-called stabilizer operators in linear time. But the simulation of large stabilizer circuits with thousands of qubits and gates, arising e.g. in the study of novel quantum error-correction protocols, still poses a challenge. In this work, we propose a GPU-based deterministic algorithm for equivalence checking of stabilizer circuits using the stabilizer tableau formalism. We explore various design choices and implement the most efficient version. Our algorithm significantly outperforms the state-of-the-art CCEC checker (which relies on the <jats:sc>Stim<\/jats:sc> simulator) in terms of time, memory, and energy. Our approach demonstrates up to two orders of magnitude speedup over existing methods. Notably, previous attempts at GPU acceleration in this area were unsuccessful, making this the first effective implementation.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_6","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:37:52Z","timestamp":1746005872000},"page":"109-128","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Parallel Equivalence Checking of Stabilizer Quantum Circuits on GPUs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5023-5348","authenticated-orcid":false,"given":"Muhammad","family":"Osama","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0719-1036","authenticated-orcid":false,"given":"Dimitrios","family":"Thanos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2433-4174","authenticated-orcid":false,"given":"Alfons","family":"Laarman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Physical Review A 70(5) (nov 2004). https:\/\/doi.org\/10.1103\/physreva.70.052328","DOI":"10.1103\/physreva.70.052328"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Amy, M.: Towards Large-scale Functional Verification of Universal Quantum Circuits. Electronic Proceedings in Theoretical Computer Science 287, 1\u201321 (Jan 2019). https:\/\/doi.org\/10.4204\/eptcs.287.1","DOI":"10.4204\/eptcs.287.1"},{"key":"6_CR3","doi-asserted-by":"publisher","unstructured":"Bal, H., Epema, D., de\u00a0Laat, C., van Nieuwpoort, R., Romein, J., Seinstra, F., Snoek, C., Wijshoff, H.: A Medium-Scale Distributed System for Computer Science Research: Infrastructure for the Long Term. IEEE Computer 49(5), 54\u201363 (2016). https:\/\/doi.org\/10.1109\/MC.2016.127","DOI":"10.1109\/MC.2016.127"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Berent, L., Burgholzer, L., Wille, R.: Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond. In: Meel, K.S., Strichman, O. (eds.) SAT 2022. LIPIcs, vol.\u00a0236, pp. 18:1\u201318:17. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2022.18","DOI":"10.4230\/LIPIcs.SAT.2022.18"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Cross, A.W., Bishop, L.S., Smolin, J.A., Gambetta, J.M.: Open Quantum Assembly Language (2017). https:\/\/doi.org\/10.48550\/arXiv.1707.03429","DOI":"10.48550\/arXiv.1707.03429"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"De Raedt, H., Jin, F., Willsch, D., Willsch, M., Yoshioka, N., Ito, N., Yuan, S., Michielsen, K.: Massively parallel quantum computer simulator, eleven years later. Computer Physics Communications 237, 47\u201361 (2019). https:\/\/doi.org\/10.1016\/j.cpc.2018.11.005","DOI":"10.1016\/j.cpc.2018.11.005"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Fowler, A.G., Mariantoni, M., Martinis, J.M., Cleland, A.N.: Surface codes: Towards practical large-scale quantum computation. Phys. Rev. A 86, 032324 (Sep 2012). https:\/\/doi.org\/10.1103\/PhysRevA.86.032324","DOI":"10.1103\/PhysRevA.86.032324"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Garcia, H.J., Markov, I.L.: Simulation of Quantum Circuits via Stabilizer Frames. IEEE Transactions on Computers 64(08), 2323\u20132336 (aug 2015). https:\/\/doi.org\/10.1109\/TC.2014.2360532","DOI":"10.1109\/TC.2014.2360532"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Gidney, C.: Stim: a fast stabilizer circuit simulator. Quantum 5, \u00a0497 (Jul 2021). https:\/\/doi.org\/10.22331\/q-2021-07-06-497","DOI":"10.22331\/q-2021-07-06-497"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"Gidney, C., Eker\u00e5, M.: How to factor 2048 bit RSA integers in 8 hours using 20 million noisy qubits. Quantum 5, \u00a0433 (Apr 2021). https:\/\/doi.org\/10.22331\/q-2021-04-15-433","DOI":"10.22331\/q-2021-04-15-433"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Google Quantum AI: Suppressing quantum errors by scaling a surface code logical qubit. Nature 614(7949), 676\u2013681 (Feb 2023). https:\/\/doi.org\/10.1038\/s41586-022-05434-1","DOI":"10.1038\/s41586-022-05434-1"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Gottesman, D.: Stabilizer Codes and Quantum Error Correction. arXiv:quant-ph\/9705052 (1997). https:\/\/doi.org\/10.48550\/arXiv.quant-ph\/9705052","DOI":"10.48550\/arXiv.quant-ph\/9705052"},{"key":"6_CR13","unstructured":"Harris, D.: Sustainable Strides: How AI and Accelerated Computing Are Driving Energy Efficiency (2024), https:\/\/blogs.nvidia.com\/blog\/accelerated-ai-energy-efficiency, accessed on July 31, 2024"},{"key":"6_CR14","unstructured":"Hashimoto, K.: GPMC (2020), https:\/\/git.trs.css.i.nagoya-u.ac.jp\/k-hasimt\/GPMC"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Hein, M., D\u00fcr, W., Eisert, J., Raussendorf, R., den Nest, M.V., Briegel, H.J.: Entanglement in Graph States and its Applications (2006). https:\/\/doi.org\/10.48550\/arXiv.quant-ph\/0602096","DOI":"10.48550\/arXiv.quant-ph\/0602096"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Javadi-Abhari, A., Treinish, M., Krsulich, K., Wood, C.J., Lishman, J., Gacon, J., Martiel, S., Nation, P.D., Bishop, L.S., Cross, A.W., Johnson, B.R., Gambetta, J.M.: Quantum computing with Qiskit (2024). https:\/\/doi.org\/10.48550\/arXiv.2405.08810","DOI":"10.48550\/arXiv.2405.08810"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Kitaev, A.Y.: Quantum computations: algorithms and error correction. Russian Mathematical Surveys 52(6), \u00a01191 (dec 1997). https:\/\/doi.org\/10.1070\/RM1997v052n06ABEH002155","DOI":"10.1070\/RM1997v052n06ABEH002155"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Litinski, D.: A Game of Surface Codes: Large-Scale Quantum Computing with Lattice Surgery (Mar 2019). https:\/\/doi.org\/10.22331\/q-2019-03-05-128","DOI":"10.22331\/q-2019-03-05-128"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Marques, J.F., Varbanov, B.M., Moreira, M.S., Ali, H., Muthusubramanian, N., Zachariadis, C., Battistel, F., Beekman, M., Haider, N., Vlothuizen, W., Bruno, A., Terhal, B.M., DiCarlo, L.: Logical-qubit operations in an error-detecting surface code. Nature Physics 18(1), 80\u201386 (Dec 2021). https:\/\/doi.org\/10.1038\/s41567-021-01423-9","DOI":"10.1038\/s41567-021-01423-9"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"McEwen, M., Bacon, D., Gidney, C.: Relaxing Hardware Requirements for Surface Code Circuits using Time-dynamics. Quantum 7, \u00a01172 (Nov 2023). https:\/\/doi.org\/10.22331\/q-2023-11-07-1172","DOI":"10.22331\/q-2023-11-07-1172"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Mei, J., Coopmans, T., Bonsangue, M., Laarman, A.: Equivalence Checking of Quantum Circuits by Model Counting. In: Benzm\u00fcller, C., Heule, M.J., Schmidt, R.A. (eds.) Automated Reasoning. pp. 401\u2013421. Springer Nature Switzerland, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63501-4_21","DOI":"10.1007\/978-3-031-63501-4_21"},{"key":"6_CR22","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press (2010)"},{"key":"6_CR23","unstructured":"NVIDIA: CUDA C Programming Guide (2024), https:\/\/docs.nvidia.com\/cuda\/cuda-c-programming-guide"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Obenland, K.M., Despain, A.M.: A Parallel Quantum Computer Simulator (1998). https:\/\/doi.org\/10.48550\/arXiv.quant-ph\/9804039","DOI":"10.48550\/arXiv.quant-ph\/9804039"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Preskill, J.: Quantum Computing in the NISQ era and beyond. Quantum 2, \u00a079 (Aug 2018). https:\/\/doi.org\/10.22331\/q-2018-08-06-79","DOI":"10.22331\/q-2018-08-06-79"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Sistla, M., Chaudhuri, S., Reps, T.: Symbolic quantum simulation with quasimodo. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 213\u2013225. Springer Nature Switzerland, Cham (2023)","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"6_CR27","unstructured":"Sutcliffe, M., Kissinger, A.: Fast classical simulation of quantum circuits via parametric rewriting in the ZX-calculus (2024)"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Terhal, B.M.: Quantum error correction for quantum memories. Rev. Mod. Phys. 87, 307\u2013346 (Apr 2015). https:\/\/doi.org\/10.1103\/RevModPhys.87.307","DOI":"10.1103\/RevModPhys.87.307"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Thanos, D., Coopmans, T., Laarman, A.: Fast Equivalence Checking of Quantum Circuits of Clifford Gates. In: Andr\u00e9, \u00c9., Sun, J. (eds.) Automated Technology for Verification and Analysis. pp. 199\u2013216. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45332-8_10","DOI":"10.1007\/978-3-031-45332-8_10"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90660-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:37:57Z","timestamp":1746005877000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}