{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,5]],"date-time":"2026-04-05T10:18:12Z","timestamp":1775384292375,"version":"3.50.1"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986840","type":"print"},{"value":"9783031986857","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,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"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>Quantum computers have advanced rapidly in qubit count and gate fidelity. However, large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC) to suppress noise. Manually or experimentally verifying the fault-tolerance property of complex QECC implementation is impractical due to the vast error combinations. This paper formalizes the fault-tolerance of QECC implementations within the language of quantum programs. By incorporating the techniques of quantum symbolic execution, we provide an automatic verification tool for quantum fault-tolerance. We evaluate and demonstrate the effectiveness of our tool on a universal set of logical operations across different QECCs.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_1","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:32:24Z","timestamp":1753155144000},"page":"3-27","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Verifying Fault-Tolerance of\u00a0Quantum Error Correction Codes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0772-6635","authenticated-orcid":false,"given":"Kean","family":"Chen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0005-2822-0448","authenticated-orcid":false,"given":"Yuhao","family":"Liu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7628-1185","authenticated-orcid":false,"given":"Wang","family":"Fang","sequence":"additional","affiliation":[]},{"given":"Jennifer","family":"Paykin","sequence":"additional","affiliation":[]},{"given":"Xin-Chuan","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Albert","family":"Schmitz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3516-1512","authenticated-orcid":false,"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6233-0334","authenticated-orcid":false,"given":"Gushu","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"052328","DOI":"10.1103\/PhysRevA.70.052328","volume":"70","author":"S Aaronson","year":"2004","unstructured":"Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Phys. Rev. A 70, 052328 (2004)","journal-title":"Phys. Rev. A"},{"key":"1_CR2","unstructured":"Acharya, R., et al.: Quantum error correction below the surface code threshold. arXiv preprint arXiv:2408.13687 (2024)"},{"issue":"7949","key":"1_CR3","doi-asserted-by":"publisher","first-page":"676","DOI":"10.1038\/s41586-022-05434-1","volume":"614","author":"R Acharya","year":"2023","unstructured":"Acharya, R., et al.: Suppressing quantum errors by scaling a surface code logical qubit. Nature 614(7949), 676\u2013681 (2023)","journal-title":"Nature"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Bauer-Marquart, F., Leue, S., Schilling, C.: symqv: automated symbolic verification of quantum programs. In: International Symposium on Formal Methods, pp. 181\u2013198. Springer (2023)","DOI":"10.1007\/978-3-031-27481-7_12"},{"issue":"1","key":"1_CR5","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1137\/141000671","volume":"59","author":"J Bezanson","year":"2017","unstructured":"Bezanson, J., Edelman, A., Karpinski, S., Shah, V.B.: Julia: a fresh approach to numerical computing. SIAM Rev. 59(1), 65\u201398 (2017)","journal-title":"SIAM Rev."},{"issue":"7997","key":"1_CR6","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1038\/s41586-023-06927-3","volume":"626","author":"D Bluvstein","year":"2023","unstructured":"Bluvstein, D., et al.: Logical quantum processor based on reconfigurable atom arrays. Nature 626(7997), 58\u201365 (2023)","journal-title":"Nature"},{"issue":"1","key":"1_CR7","doi-asserted-by":"publisher","first-page":"012305","DOI":"10.1103\/PhysRevA.76.012305","volume":"76","author":"H Bomb\u00edn","year":"2007","unstructured":"Bomb\u00edn, H., Martin-Delgado, M.A.: Optimal resources for topological two-dimensional stabilizer codes: Comparative study. Phys. Rev. A-Atomic, Mol. Opt. Phys. 76(1), 012305 (2007)","journal-title":"Phys. Rev. A-Atomic, Mol. Opt. Phys."},{"issue":"18","key":"1_CR8","doi-asserted-by":"publisher","first-page":"180501","DOI":"10.1103\/PhysRevLett.97.180501","volume":"97","author":"H Bombin","year":"2006","unstructured":"Bombin, H., Martin-Delgado, M.A.: Topological quantum distillation. Phys. Rev. Lett. 97(18), 180501 (2006)","journal-title":"Phys. Rev. Lett."},{"issue":"2","key":"1_CR9","doi-asserted-by":"publisher","first-page":"022316","DOI":"10.1103\/PhysRevA.71.022316","volume":"71","author":"S Bravyi","year":"2005","unstructured":"Bravyi, S., Kitaev, A.: Universal quantum computation with ideal clifford gates and noisy ancillas. Phys. Rev. A-Atomic Mol. Opt. Phys. 71(2), 022316 (2005)","journal-title":"Phys. Rev. A-Atomic Mol. Opt. Phys."},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Breuckmann, N.P., Eberhardt, J.N.: Quantum low-density parity-check codes. PRX Quant. 2(4) (2021)","DOI":"10.1103\/PRXQuantum.2.040101"},{"issue":"9","key":"1_CR11","doi-asserted-by":"publisher","first-page":"1810","DOI":"10.1109\/TCAD.2020.3032630","volume":"40","author":"L Burgholzer","year":"2021","unstructured":"Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 40(9), 1810\u20131824 (2021)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Burgholzer, L., Wille, R.: Handling non-unitaries in quantum circuit equivalence checking. In: Proceedings of the 59th ACM\/IEEE Design Automation Conference, DAC 2022, ACM (2022)","DOI":"10.1145\/3489517.3530482"},{"key":"1_CR13","unstructured":"Chen, K., et al.: Verifying fault-tolerance of quantum error correction codes (extended version). arXiv preprint arXiv:2501.14380 (2025)"},{"issue":"6","key":"1_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3689333","volume":"29","author":"K Chen","year":"2024","unstructured":"Chen, K., Ying, M.: Automatic test pattern generation for robust quantum circuit testing. ACM Trans. Des. Autom. Electron. Syst. 29(6), 1\u201336 (2024)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"issue":"3","key":"1_CR15","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0024-3795(75)90075-0","volume":"10","author":"MD Choi","year":"1975","unstructured":"Choi, M.D.: Completely positive linear maps on complex matrices. Linear Algebra Appl. 10(3), 285\u2013290 (1975)","journal-title":"Linear Algebra Appl."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Fang, W., Ying, M.: Symbolic execution for quantum error correction programs. Proc. ACM Program. Lang. 8(PLDI), 1040\u20131065 (2024)","DOI":"10.1145\/3656419"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Fang, W., Ying, M.: Symphase: phase symbolization for fast simulation of stabilizer circuits. In: Proceedings of the 61st ACM\/IEEE Design Automation Conference, pp.\u00a01\u20136 (2024)","DOI":"10.1145\/3649329.3655902"},{"issue":"4","key":"1_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3456877","volume":"2","author":"Y Feng","year":"2021","unstructured":"Feng, Y., Ying, M.: Quantum hoare logic with classical variables. ACM Trans. Quant. Comput. 2(4), 1\u201343 (2021)","journal-title":"ACM Trans. Quant. Comput."},{"issue":"6","key":"1_CR19","doi-asserted-by":"publisher","first-page":"062329","DOI":"10.1103\/PhysRevA.88.062329","volume":"88","author":"J Ghosh","year":"2013","unstructured":"Ghosh, J., Fowler, A.G., Martinis, J.M., Geller, M.R.: Understanding the effects of leakage in superconducting quantum-error-detection circuits. Phys. Rev. A 88(6), 062329 (2013)","journal-title":"Phys. Rev. A"},{"key":"1_CR20","unstructured":"Gottesman, D.: Stabilizer Codes and Quantum Error Correction. California Institute of Technology (1997)"},{"key":"1_CR21","unstructured":"Gottesman, D.: The heisenberg representation of quantum computers. arXiv preprint quant-ph\/9807006 (1998)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Gottesman, D.: An introduction to quantum error correction and fault-tolerant quantum computation. In: Quantum Information Science and Its Contributions to Mathematics, Proceedings of Symposia in Applied Mathematics, vol.\u00a068 (2010)","DOI":"10.1090\/psapm\/068\/2762145"},{"key":"1_CR23","unstructured":"Gottesman, D.: Surviving as a quantum computer in a classical world. Textbook manuscript preprint (2024)"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Guan, J., Feng, Y., Turrini, A., Ying, M.: Measurement-based verification of quantum markov chains. In: International Conference on Computer Aided Verification, pp. 533\u2013554. Springer (2024)","DOI":"10.1007\/978-3-031-65633-0_24"},{"key":"1_CR25","unstructured":"Hietala, K., Rand, R., Hung, S.H., Li, L., Hicks, M.: Proving quantum programs correct. arXiv preprint arXiv:2010.01240 (2020)"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Hong, X., Ying, M., Feng, Y., Zhou, X., Li, S.: Approximate equivalence checking of noisy quantum circuits. In: 2021 58th ACM\/IEEE Design Automation Conference (DAC), pp. 637\u2013642. IEEE (2021)","DOI":"10.1109\/DAC18074.2021.9586214"},{"issue":"12","key":"1_CR27","doi-asserted-by":"publisher","first-page":"123011","DOI":"10.1088\/1367-2630\/14\/12\/123011","volume":"14","author":"D Horsman","year":"2012","unstructured":"Horsman, D., Fowler, A.G., Devitt, S., Van Meter, R.: Surface code quantum computing by lattice surgery. New J. Phys. 14(12), 123011 (2012)","journal-title":"New J. Phys."},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Hung, S.H., Hietala, K., Zhu, S., Ying, M., Hicks, M., Wu, X.: Quantitative robustness analysis of quantum programs. Proc. ACM Program. Lang. 3(POPL), 1\u201329 (2019)","DOI":"10.1145\/3290344"},{"key":"1_CR29","unstructured":"Hung, S.H., Peng, Y., Wang, X., Zhu, S., Wu, X.: On the theory and practice of invariant-based verification of quantum programs (2019), https:\/\/api.semanticscholar.org\/CorpusID:208634831"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Jamio\u0142kowski, A.: Linear transformations which preserve trace and positive semidefiniteness of operators. Rep. Math. Phys. 3(4) (1972)","DOI":"10.1016\/0034-4877(72)90011-0"},{"issue":"1","key":"1_CR31","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/S0003-4916(02)00018-0","volume":"303","author":"A Kitaev","year":"2003","unstructured":"Kitaev, A.: Fault-tolerant quantum computation by anyons. Ann. Phys. 303(1), 2\u201330 (2003)","journal-title":"Ann. Phys."},{"key":"1_CR32","unstructured":"Knill, E.: Fault-tolerant postselected quantum computation: Schemes. arXiv preprint quant-ph\/0402171 (2004)"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Leverrier, A., Z\u00e9mor, G.: Quantum tanner codes. In: 2022 IEEE 63rd Annual Symposium on Foundations of Computer Science (FOCS), pp. 872\u2013883. IEEE (2022)","DOI":"10.1109\/FOCS54457.2022.00117"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Li, G., Zhou, L., Yu, N., Ding, Y., Ying, M., Xie, Y.: Projection-based runtime assertions for testing and debugging quantum programs. Proc. ACM Program. Lang. 4(OOPSLA), 1\u201329 (2020)","DOI":"10.1145\/3428218"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Liu, J., et al.: Formal verification of quantum algorithms using quantum hoare logic, pp. 187\u2013207. Computer Aided Verification (2019)","DOI":"10.1007\/978-3-030-25543-5_12"},{"issue":"10","key":"1_CR36","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s11128-023-04144-5","volume":"22","author":"J Nan","year":"2023","unstructured":"Nan, J., Zichen, W., Jian, W.: Quantum symbolic execution. Quant. Inf. Process. 22(10), 389 (2023)","journal-title":"Quant. Inf. Process."},{"issue":"1","key":"1_CR37","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1023\/A:1011233615437","volume":"24","author":"G Nebe","year":"2001","unstructured":"Nebe, G., Rains, E.M., Sloane, N.J.: The invariants of the clifford groups. Des. Codes Crypt. 24(1), 99\u2013122 (2001)","journal-title":"Des. Codes Crypt."},{"key":"1_CR38","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press (2010)"},{"key":"1_CR39","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 3\u201317. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_1, https:\/\/doi.org\/10.1007\/978-3-031-37703-7_1","DOI":"10.1007\/978-3-031-37703-7_1"},{"issue":"1","key":"1_CR40","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1145\/3093333.3009894","volume":"52","author":"J Paykin","year":"2017","unstructured":"Paykin, J., Rand, R., Zdancewic, S.: Qwire: a core language for quantum circuits. ACM SIGPLAN Notices 52(1), 846\u2013858 (2017)","journal-title":"ACM SIGPLAN Notices"},{"issue":"3","key":"1_CR41","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1109\/JETCAS.2022.3202204","volume":"12","author":"T Peham","year":"2022","unstructured":"Peham, T., Burgholzer, L., Wille, R.: Equivalence checking of quantum circuits with the zx-calculus. IEEE J. Emerg. Sel. Top. Circ. Syst. 12(3), 662\u2013675 (2022)","journal-title":"IEEE J. Emerg. Sel. Top. Circ. Syst."},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Peham, T., Burgholzer, L., Wille, R.: Equivalence checking of parameterized quantum circuits: verifying the compilation of variational quantum algorithms. In: Proceedings of the 28th Asia and South Pacific Design Automation Conference, ASPDAC 2023, pp. 702\u2013708. ACM, New York, NY, USA (2023)","DOI":"10.1145\/3566097.3567932"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Preskill, J.: Quantum computing 40 years later. In: Feynman Lectures on Computation, pp. 193\u2013244. CRC Press (2023)","DOI":"10.1201\/9781003358817-7"},{"key":"1_CR44","unstructured":"Reichardt, B.W., et al.: Logical computation demonstrated with a neutral atom quantum processor. arXiv preprint arXiv:2411.11822 (2024)"},{"key":"1_CR45","unstructured":"Rodriguez, P.S., et\u00a0al.: Experimental demonstration of logical magic state distillation. arXiv preprint arXiv:2412.15165 (2024)"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Sawicki, A., Karnas, K.: Universality of single-qudit gates. In: Annales Henri Poincar\u00e9, vol.\u00a018, pp. 3515\u20133552. Springer (2017)","DOI":"10.1007\/s00023-017-0604-z"},{"key":"1_CR47","doi-asserted-by":"publisher","first-page":"1291","DOI":"10.1007\/s11390-021-1637-9","volume":"36","author":"WJ Shi","year":"2021","unstructured":"Shi, W.J., Cao, Q.X., Deng, Y.X., Jiang, H.R., Feng, Y.: Symbolic reasoning about quantum circuits in Coq. J. Comput. Sci. Technol. 36, 1291\u20131306 (2021)","journal-title":"J. Comput. Sci. Technol."},{"key":"1_CR48","unstructured":"Shi, Y., et al.: Certiq: a mostly-automated verification of a realistic quantum compiler. arXiv preprint arXiv:1908.08963 (2019)"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Shor, P.W.: Fault-tolerant quantum computation. In: Proceedings of 37th Conference on Foundations of Computer Science, pp. 56\u201365. IEEE (1996)","DOI":"10.1109\/SFCS.1996.548464"},{"issue":"5","key":"1_CR50","doi-asserted-by":"publisher","first-page":"1701","DOI":"10.1109\/18.771249","volume":"45","author":"AM Steane","year":"1999","unstructured":"Steane, A.M.: Quantum reed-muller codes. IEEE Trans. Inf. Theory 45(5), 1701\u20131703 (1999)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"Suchara, M., Cross, A.W., Gambetta, J.M.: Leakage suppression in the toric code. In: 2015 IEEE International Symposium on Information Theory (ISIT), pp. 1119\u20131123. IEEE (2015)","DOI":"10.1109\/ISIT.2015.7282629"},{"key":"1_CR52","unstructured":"Tamiya, S., Koashi, M., Yamasaki, H.: Polylog-time-and constant-space-overhead fault-tolerant quantum computation with quantum low-density parity-check codes. arXiv preprint arXiv:2411.03683 (2024)"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Tao, R., Shi, Y., Yao, J., Hui, J., Chong, F.T., Gu, R.: Gleipnir: toward practical error analysis for quantum programs. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pp. 48\u201364. ACM, New York, NY, USA (2021)","DOI":"10.1145\/3453483.3454029"},{"key":"1_CR54","doi-asserted-by":"crossref","unstructured":"Tao, R., et al.: Giallar: push-button verification for the qiskit quantum compiler. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022, pp. 641\u2013656. ACM, New York, NY, USA (2022)","DOI":"10.1145\/3519939.3523431"},{"issue":"9","key":"1_CR55","doi-asserted-by":"publisher","first-page":"3143","DOI":"10.1109\/TCAD.2021.3117506","volume":"41","author":"Q Wang","year":"2022","unstructured":"Wang, Q., Li, R., Ying, M.: Equivalence checking of sequential quantum circuits. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(9), 3143\u20133156 (2022)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"6","key":"1_CR56","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2049706.2049708","volume":"33","author":"M Ying","year":"2012","unstructured":"Ying, M.: Floyd-hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 33(6), 1\u201349 (2012)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"Ying, M.: A practical quantum hoare logic with classical variables, i. arXiv preprint arXiv:2412.09869 (2024)","DOI":"10.2139\/ssrn.5193712"},{"issue":"4","key":"1_CR58","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1109\/TSE.2010.94","volume":"37","author":"M Ying","year":"2010","unstructured":"Ying, M., Feng, Y.: A flowchart language for quantum programming. IEEE Trans. Softw. Eng. 37(4), 466\u2013485 (2010)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"Ying, M., Ying, S., Wu, X.: Invariants of quantum programs: characterisations and generation. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 818\u2013832. ACM, New York, NY, USA (2017)","DOI":"10.1145\/3009837.3009840"},{"key":"1_CR60","doi-asserted-by":"crossref","unstructured":"Zhou, L., Barthe, G., Strub, P.Y., Liu, J., Ying, M.: CoqQ: foundational verification of quantum programs. Proc. ACM Program. Lang. 7(POPL) (2023)","DOI":"10.1145\/3571222"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T08:55:15Z","timestamp":1760086515000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_1","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":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","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":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}