{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,30]],"date-time":"2026-08-30T01:08:41Z","timestamp":1788052121437,"version":"build-2784847793"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906596","type":"print"},{"value":"9783031906602","type":"electronic"}],"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>, originally developed as the first exact quantum circuit simulator, is extended in this paper to provide capabilities for the analysis and verification of quantum states. It provides an interface for users to specify interested quantum states for querying the exact probability or expectation value of a user-defined property. Case studies on three quantum algorithms show the unique capability of  benefiting exact quantum circuit analysis and verification, beyond the support by other tools.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_7","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:37:41Z","timestamp":1746005861000},"page":"129-138","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["SliQSim: A Quantum Circuit Simulator and Solver for Probability and Statistics Queries"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-5947-6206","authenticated-orcid":false,"given":"Tian-Fu","family":"Chen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2279-4732","authenticated-orcid":false,"given":"Jie-Hong R.","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Amy, M.: Towards large-scale functional verification of universal quantum circuits. arXiv preprint arXiv:1805.06908 (2018)","DOI":"10.4204\/EPTCS.287.1"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Bauer-Marquart, F., Leue, S., Schilling, C.: symQV: Automated symbolic verification of quantum programs. In: Int. Symp. on Formal Methods. pp. 181\u2013198. Springer (2023)","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Comput. 100(8), 677\u2013691 (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Trans. on Comput.-Aided Design Integr. Circuits Syst. 40(9), 1810\u20131824 (2021)","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Chen, T.F., Chen, Y.F., Jiang, J.H.R., Jobranov\u00e1, S., Leng\u00e1l, O.: Accelerating quantum circuit simulation with symbolic execution and loop summarization. In: Proc. ICCAD (2024)","DOI":"10.1145\/3676536.3676711"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Chen, T.F., Jiang, J.H.R.: Boolean matching reversible circuits: Algorithm and complexity. In: Proc. DAC (2024)","DOI":"10.1145\/3649329.3657312"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Chen, T.F., Jiang, J.H.R., Hsieh, M.H.: Partial equivalence checking of quantum circuits. In: Proc. QCE. pp. 594\u2013604 (2022)","DOI":"10.1109\/QCE53715.2022.00082"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Chen, Y.F., Chung, K.M., Leng\u00e1l, O., Lin, J.A., Tsai, W.L.: AutoQ: An automata-based quantum circuit verifier. In: Proc. CAV. pp. 139\u2013153. Springer (2023)","DOI":"10.1007\/978-3-031-37709-9_7"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Grover, L.K.: A fast quantum mechanical algorithm for database search. In: Proc. STOC. pp. 212\u2013219 (1996)","DOI":"10.1145\/237814.237866"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Incudini, M., Tarocco, F., Mengoni, R., Di\u00a0Pierro, A., Mandarino, A.: Computing graph edit distance on quantum devices. Quantum Mach. Intell. 4(2), \u00a024 (2022)","DOI":"10.1007\/s42484-022-00077-x"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Kandala, A., Mezzacapo, A., Temme, K., Takita, M., Brink, M., Chow, J.M., Gambetta, J.M.: Hardware-efficient variational quantum eigensolver for small molecules and quantum magnets. Nature 549(7671), 242\u2013246 (2017)","DOI":"10.1038\/nature23879"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Kissinger, A., van\u00a0de Wetering, J.: Simulating quantum circuits with ZX-calculus reduced stabiliser decompositions. Quantum Sci. and Technol. 7(4), 044001 (2022)","DOI":"10.1088\/2058-9565\/ac5d20"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Li, X., Kulkarni, V., Chen, D.T., Guan, Q., Jiang, W., Xie, N., Xu, S., Chaudhary, V.: Efficient circuit wire cutting based on commuting groups. In: Proc. QCE (2024)","DOI":"10.1109\/QCE60285.2024.00023"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Mei, J., Bonsangue, M., Laarman, A.: Simulating quantum circuits by model counting. In: Proc. CAV. pp. 555\u2013578. Springer (2024)","DOI":"10.1007\/978-3-031-65633-0_25"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Peng, T., Harrow, A.W., Ozols, M., Wu, X.: Simulating large quantum circuits on a small quantum computer. Physical review letters 125(15), 150504 (2020)","DOI":"10.1103\/PhysRevLett.125.150504"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Simon, D.R.: On the power of quantum computation. SIAM J. on Comput. 26(5), 1474\u20131483 (1997)","DOI":"10.1137\/S0097539796298637"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Sistla, M., Chaudhuri, S., Reps, T.: Symbolic quantum simulation with Quasimodo. In: Proc. CAV. pp. 213\u2013225. Springer (2023)","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Tang, W., Tomesh, T., Suchara, M., Larson, J., Martonosi, M.: CutQC: using small quantum computers for large quantum circuit evaluations. In: Proc. ASPLOS. pp. 473\u2013486 (2021)","DOI":"10.1145\/3445814.3446758"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Tsai, Y.H., Jiang, J.H.R., Jhang, C.S.: Bit-slicing the Hilbert space: Scaling up accurate quantum circuit simulation. In: Proc. DAC. pp. 439\u2013444 (2021)","DOI":"10.1109\/DAC18074.2021.9586191"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Wei, C.Y., Tsai, Y.H., Jhang, C.S., Jiang, J.H.R.: Accurate BDD-based unitary operator manipulation for scalable and robust quantum circuit verification. In: Proc. DAC. pp. 523\u2013528 (2022)","DOI":"10.1145\/3489517.3530481"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Wierichs, D., Gogolin, C., Kastoryano, M.: Avoiding local minima in variational quantum eigensolvers with the natural gradient optimizer. Physical Review Research 2(4), 043246 (2020)","DOI":"10.1103\/PhysRevResearch.2.043246"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Ying, M., Feng, Y.: Model checking quantum systems: Principles and algorithms. Cambridge University Press (2021)","DOI":"10.1017\/9781108613323"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proc. PLDI. pp. 542\u2013558 (2021)","DOI":"10.1145\/3453483.3454061"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Zhang, S.X., Allcock, J., Wan, Z.Q., Liu, S., Sun, J., Yu, H., Yang, X.H., Qiu, J., Ye, Z., Chen, Y.Q., et\u00a0al.: TensorCircuit: a quantum software framework for the NISQ era. Quantum 7, \u00a0912 (2023)","DOI":"10.22331\/q-2023-02-02-912"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Zulehner, A., Wille, R.: Advanced simulation of quantum computations. IEEE Trans. on Comput.-Aided Des. of Integr. Circuits and Syst. 38(5), 848\u2013859 (2018)","DOI":"10.1109\/TCAD.2018.2834427"}],"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_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:37:55Z","timestamp":1746005875000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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"}}]}}