{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:12:56Z","timestamp":1784837576649,"version":"3.55.0"},"publisher-location":"Cham","reference-count":63,"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>Applications of decision diagrams in quantum circuit analysis have been an active research area. Our work introduces FeynmanDD, a new method utilizing standard and multi-terminal decision diagrams for quantum circuit simulation and equivalence checking. Unlike previous approaches that exploit patterns in quantum states and operators, our method explores useful structures in the path integral formulation, essentially transforming the analysis into a counting problem. The method then employs efficient counting algorithms using decision diagrams as its underlying computational engine. Through comprehensive theoretical analysis and numerical experiments, we demonstrate FeynmanDD\u2019s capabilities and limitations in quantum circuit analysis, highlighting the value of this new BDD-based approach.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_2","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:31:35Z","timestamp":1753155095000},"page":"28-52","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["FeynmanDD: Quantum Circuit Analysis with\u00a0Classical Decision Diagrams"],"prefix":"10.1007","author":[{"given":"Ziyuan","family":"Wang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bin","family":"Cheng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Longxiang","family":"Yuan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhengfeng","family":"Ji","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"issue":"1","key":"2_CR1","doi-asserted-by":"publisher","first-page":"143","DOI":"10.4086\/toc.2013.v009a004","volume":"9","author":"S Aaronson","year":"2013","unstructured":"Aaronson, S., Arkhipov, A.: The computational complexity of linear optics. Theory Comput. 9(1), 143\u2013252 (2013). https:\/\/doi.org\/10.4086\/toc.2013.v009a004","journal-title":"Theory Comput."},{"issue":"5","key":"2_CR2","doi-asserted-by":"publisher","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(5), 052328 (2004). https:\/\/doi.org\/10.1103\/PhysRevA.70.052328","journal-title":"Phys. Rev. A"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Abdollahi, A., Pedram, M.: Analysis and synthesis of quantum circuits by using quantum decision diagrams. In: Proceedings of the Design Automation & Test in Europe Conference, pp.\u00a01\u20136. IEEE, Munich, Germany (2006). https:\/\/doi.org\/10.1109\/date.2006.244176","DOI":"10.1109\/date.2006.244176"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., et al.: Verifying quantum circuits with level-synchronized tree automata. Verifying Quantum Circuits Level-Synchronized Tree Autom. 9(POPL), 32:923\u201332:953 (2025). https:\/\/doi.org\/10.1145\/3704868","DOI":"10.1145\/3704868"},{"key":"2_CR5","unstructured":"Amy, M.: Formal Methods in Quantum Circuit Design. Ph.D. thesis, University of Waterloo (2019)"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.287.1","volume":"287","author":"M Amy","year":"2019","unstructured":"Amy, M.: Towards large-scale functional verification of universal quantum circuits. Electron. Proc. Theoret. Comput. Sci. 287, 1\u201321 (2019). https:\/\/doi.org\/10.4204\/EPTCS.287.1","journal-title":"Electron. Proc. Theoret. Comput. Sci."},{"key":"2_CR7","doi-asserted-by":"publisher","first-page":"127","DOI":"10.4204\/eptcs.384.8","volume":"384","author":"M Amy","year":"2023","unstructured":"Amy, M.: Complete equational theories for the sum-over-paths with unbalanced amplitudes. Electron. Proc. Theoret. Comput. Sci. 384, 127\u2013141 (2023). https:\/\/doi.org\/10.4204\/eptcs.384.8","journal-title":"Electron. Proc. Theoret. Comput. Sci."},{"issue":"7779","key":"2_CR8","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1038\/s41586-019-1666-5","volume":"574","author":"F Arute","year":"2019","unstructured":"Arute, F., et al.: Quantum supremacy using a programmable superconducting processor. Nature 574(7779), 505\u2013510 (2019). https:\/\/doi.org\/10.1038\/s41586-019-1666-5","journal-title":"Nature"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Bahar, R., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD), pp. 188\u2013191. IEEE Comput. Soc. Press, Santa Clara, CA, USA (1993). https:\/\/doi.org\/10.1109\/iccad.1993.580054","DOI":"10.1109\/iccad.1993.580054"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/tc.1986.1676819","DOI":"10.1109\/tc.1986.1676819"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Bryant, R.: Binary decision diagrams and beyond: enabling technologies for formal verification. In: Proceedings of IEEE International Conference on Computer Aided Design (ICCAD), pp. 236\u2013243. IEEE Comput. Soc. Press, San Jose, CA, USA (1995). https:\/\/doi.org\/10.1109\/iccad.1995.480018","DOI":"10.1109\/iccad.1995.480018"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Burgholzer, L., Bauer, H., Wille, R.: Hybrid Schr\u00f6dinger-feynman simulation of quantum circuits with decision diagrams. In: 2021 IEEE International Conference on Quantum Computing and Engineering (QCE), pp. 199\u2013206. IEEE, Broomfield, CO, USA (2021). https:\/\/doi.org\/10.1109\/QCE52317.2021.00037","DOI":"10.1109\/QCE52317.2021.00037"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit-building quantum programs. In: Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, pp. 148\u2013177. Springer-Verlag, Berlin, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_6","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Chen, Y.F., Chung, K.M., Leng\u00e1l, O., Lin, J.A., Tsai, W.L.: AutoQ: an automata-based quantum circuit verifier. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 139\u2013153. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_7","DOI":"10.1007\/978-3-031-37709-9_7"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Coecke, B., Duncan, R.: Interacting quantum observables. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) Automata, Languages and Programming, pp. 298\u2013310. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70583-3_25","DOI":"10.1007\/978-3-540-70583-3_25"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Coecke, B., Horsman, D., Kissinger, A., Wang, Q.: Kindergarden quantum mechanics graduates...or how I learned to stop gluing LEGO together and love the ZX-calculus. Theoret. Comput. Sci. 897, 1\u201322 (2022). https:\/\/doi.org\/10.1016\/j.tcs.2021.07.024","DOI":"10.1016\/j.tcs.2021.07.024"},{"key":"2_CR17","unstructured":"Dawson, C.: Solovay Kitaev algorithm (2019)"},{"issue":"2","key":"2_CR18","first-page":"102","volume":"5","author":"CM Dawson","year":"2005","unstructured":"Dawson, C.M., Hines, A.P., Mortimer, D., Haselgrove, H.L., Nielsen, M.A., Osborne, T.J.: Quantum computing and polynomial equations over the finite field Z2. Quantum Info. Comput. 5(2), 102\u2013112 (2005)","journal-title":"Quantum Info. Comput."},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Deng, H., Tao, R., Peng, Y., Wu, X.: A case for synthesis of recursive quantum unitary programs. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632901","DOI":"10.1145\/3632901"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"van Dijk, T.: Sylvan: multi-core decision diagrams. PhD, University of Twente, Enschede, The Netherlands (2016). https:\/\/doi.org\/10.3990\/1.9789036541602","DOI":"10.3990\/1.9789036541602"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Fenner, S., Green, F., Homer, S., Pruim, R.: Determining acceptance possibility for a quantum computation is hard for the polynomial hierarchy. Proc. R. Soc. London. Series A: Math. Phys. Eng. Sci. 455(1991), 3953\u20133966 (1999). https:\/\/doi.org\/10.1098\/rspa.1999.0485","DOI":"10.1098\/rspa.1999.0485"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Ferrara, A., Pan, G., Vardi, M.Y.: Treewidth in verification: local vs. global. In: Sutcliffe, G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 489\u2013503. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11591191_34","DOI":"10.1007\/11591191_34"},{"key":"2_CR23","unstructured":"Feynman, R., Hibbs, A.: Quantum Mechanics and Path Integrals. International series in pure and applied physic, McGraw-Hill (1965)"},{"issue":"3","key":"2_CR24","doi-asserted-by":"publisher","DOI":"10.1103\/physreva.87.032332","volume":"87","author":"B Giles","year":"2013","unstructured":"Giles, B., Selinger, P.: Exact synthesis of multiqubit Clifford+ T circuits. Phys. Rev. A 87(3), 032332 (2013). https:\/\/doi.org\/10.1103\/physreva.87.032332","journal-title":"Phys. Rev. A"},{"key":"2_CR25","unstructured":"Gottesman, D.: The Heisenberg Representation of Quantum Computers. arXiv:quant-ph\/9807006 (1998)"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Hillmich, S., Zulehner, A., Kueng, R., Markov, I.L., Wille, R.: Approximating decision diagrams for quantum circuit simulation. ACM Trans. Quantum Comput. 3(4), 22:1\u201322:21 (2022). https:\/\/doi.org\/10.1145\/3530776","DOI":"10.1145\/3530776"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Hong, X., Feng, Y., Li, S., Ying, M.: Equivalence checking of dynamic quantum circuits. In: 2022 IEEE\/ACM International Conference On Computer Aided Design (ICCAD), pp.\u00a01\u20138 (2022)","DOI":"10.1145\/3508352.3549479"},{"key":"2_CR28","doi-asserted-by":"publisher","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 (2021). https:\/\/doi.org\/10.1109\/DAC18074.2021.9586214","DOI":"10.1109\/DAC18074.2021.9586214"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Hong, X., Zhou, X., Li, S., Feng, Y., Ying, M.: A tensor network based decision diagram for representation of quantum circuits. ACM Trans. Des. Autom. Electron. Syst. 27(6), 60:1\u201360:30 (2022). https:\/\/doi.org\/10.1145\/3514355","DOI":"10.1145\/3514355"},{"key":"2_CR30","doi-asserted-by":"publisher","unstructured":"Jiang, S., Fu, R., Burgholzer, L., Wille, R., Ho, T.Y., Huang, T.W.: FlatDD: a high-performance quantum circuit simulator using decision diagram and flat array. In: Proceedings of the 53rd International Conference on Parallel Processing, pp. 388\u2013399. ICPP \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3673038.3673073","DOI":"10.1145\/3673038.3673073"},{"key":"2_CR31","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 4, Fascicle 1 (Bitwise Tricks & Techniques; Binary Decision Diagrams). AddisonWesley Professional, Upper Saddle River, NJ, 1 edition edn. (2009)"},{"issue":"12","key":"2_CR32","doi-asserted-by":"publisher","first-page":"1058","DOI":"10.3390\/e26121058","volume":"26","author":"CB Larsen","year":"2024","unstructured":"Larsen, C.B., Olsen, S.B., Larsen, K.G., Schilling, C.: Contraction heuristics for tensor decision diagrams. Entropy 26(12), 1058 (2024). https:\/\/doi.org\/10.3390\/e26121058","journal-title":"Entropy"},{"issue":"4","key":"2_CR33","doi-asserted-by":"publisher","first-page":"805","DOI":"10.1109\/TPDS.2019.2947511","volume":"31","author":"R Li","year":"2020","unstructured":"Li, R., Wu, B., Ying, M., Sun, X., Yang, G.: Quantum supremacy circuit simulation on sunway Taihulight. IEEE Trans. Parallel Distrib. Syst. 31(4), 805\u2013816 (2020). https:\/\/doi.org\/10.1109\/TPDS.2019.2947511","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"2_CR34","unstructured":"Lind-Nielsen, J.: Buddy: A binary decision diagram package (1999)"},{"issue":"10","key":"2_CR35","doi-asserted-by":"publisher","first-page":"1377","DOI":"10.1109\/TC.2011.114","volume":"60","author":"CY Lu","year":"2011","unstructured":"Lu, C.Y., Wang, S.A., Kuo, S.Y.: An extended XQDD representation for multiple-valued quantum logic. IEEE Trans. Comput. 60(10), 1377\u20131389 (2011). https:\/\/doi.org\/10.1109\/TC.2011.114","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"2_CR36","doi-asserted-by":"publisher","first-page":"963","DOI":"10.1137\/050644756","volume":"38","author":"IL Markov","year":"2008","unstructured":"Markov, I.L., Shi, Y.: Simulating quantum computation by contracting tensor networks. SIAM J. Comput. 38(3), 963\u2013981 (2008). https:\/\/doi.org\/10.1137\/050644756","journal-title":"SIAM J. Comput."},{"key":"2_CR37","doi-asserted-by":"publisher","unstructured":"Mei, J., Bonsangue, M., Laarman, A.: Simulating Quantum Circuits by Model Counting (2024). https:\/\/doi.org\/10.48550\/arXiv.2403.07197","DOI":"10.48550\/arXiv.2403.07197"},{"key":"2_CR38","volume-title":"Equivalence Checking of Digital Circuits: Fundamentals, Principles","author":"P Molitor","year":"2004","unstructured":"Molitor, P., Mohnke, J., Becker, B., Scholl, C.: Equivalence Checking of Digital Circuits: Fundamentals, Principles. Methods. Springer, New York, NY (2004)"},{"issue":"8","key":"2_CR39","doi-asserted-by":"publisher","DOI":"10.1088\/1751-8121\/aa565f","volume":"50","author":"A Montanaro","year":"2017","unstructured":"Montanaro, A.: Quantum circuits and low-degree polynomials over F2. J. Phys. A: Math. Theor. 50(8), 084002 (2017). https:\/\/doi.org\/10.1088\/1751-8121\/aa565f","journal-title":"J. Phys. A: Math. Theor."},{"key":"2_CR40","doi-asserted-by":"publisher","unstructured":"Nam, Y., Ross, N.J., Su, Y., Childs, A.M., Maslov, D.: Automated optimization of large quantum circuits with continuous parameters. NPJ Quantum Inf. 4(1), 1\u201312 (2018). https:\/\/doi.org\/10.1038\/s41534-018-0072-4","DOI":"10.1038\/s41534-018-0072-4"},{"issue":"1","key":"2_CR41","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1109\/tcad.2015.2459034","volume":"35","author":"P Niemann","year":"2016","unstructured":"Niemann, P., Wille, R., Miller, D.M., Thornton, M.A., Drechsler, R.: QMDDs: efficient quantum function representation and manipulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 35(1), 86\u201399 (2016). https:\/\/doi.org\/10.1109\/tcad.2015.2459034","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"3","key":"2_CR42","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.128.030501","volume":"128","author":"F Pan","year":"2022","unstructured":"Pan, F., Zhang, P.: Simulation of quantum circuits using the big-batch tensor network method. Phys. Rev. Lett. 128(3), 030501 (2022). https:\/\/doi.org\/10.1103\/PhysRevLett.128.030501","journal-title":"Phys. Rev. Lett."},{"issue":"3","key":"2_CR43","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). https:\/\/doi.org\/10.1109\/JETCAS.2022.3202204","journal-title":"IEEE J. Emerg. Sel. Top. Circ. Syst."},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Ross, N.J., Selinger, P.: Optimal ancilla-free Clifford+T approximation of z-rotations. arXiv:1403.2975 [quant-ph] (2016)","DOI":"10.26421\/QIC16.11-12-1"},{"key":"2_CR45","doi-asserted-by":"publisher","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD), pp. 42\u201347 (1993). https:\/\/doi.org\/10.1109\/ICCAD.1993.580029","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"2_CR46","doi-asserted-by":"publisher","unstructured":"Sistla, M., Chaudhuri, S., Reps, T.: Symbolic quantum simulation with quasimodo. In: Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17\u201322, 2023, Proceedings, Part III, pp. 213\u2013225. Springer-Verlag, Berlin, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_11","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"2_CR47","doi-asserted-by":"publisher","unstructured":"Sistla, M., Chaudhuri, S., Reps, T.: Weighted context-free-language ordered binary decision diagrams. Weighted CFLOBDDs 8(OOPSLA2), 320:1390\u2013320:1419 (2024). https:\/\/doi.org\/10.1145\/3689760","DOI":"10.1145\/3689760"},{"key":"2_CR48","doi-asserted-by":"crossref","unstructured":"S\u00f8lvsten, S.C., van\u00a0de Pol, J., Jakobsen, A.B., Thomasen, M.W.B.: Efficient Binary Decision Diagram Manipulation in External Memory. arXiv:2104.12101 [cs] (2021)","DOI":"10.1007\/978-3-030-99527-0_16"},{"key":"2_CR49","unstructured":"Somenzi, F.: CUDD: CU decision diagram package (release 3.0.0). University of Colorado at Boulder (2005)"},{"key":"2_CR50","doi-asserted-by":"publisher","unstructured":"Tsai, Y.H., Jiang, J.H.R., Jhang, C.S.: Bit-slicing the Hilbert space: scaling up accurate quantum circuit simulation. In: 2021 58th ACM\/IEEE Design Automation Conference (DAC), pp. 439\u2013444 (2021). https:\/\/doi.org\/10.1109\/DAC18074.2021.9586191","DOI":"10.1109\/DAC18074.2021.9586191"},{"issue":"5","key":"2_CR51","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1023\/b:qinp.0000022725.70000.4a","volume":"2","author":"GF Viamontes","year":"2003","unstructured":"Viamontes, G.F., Markov, I.L., Hayes, J.P.: Improving gate-level simulation of quantum circuits. Quantum Inf. Process. 2(5), 347\u2013380 (2003). https:\/\/doi.org\/10.1023\/b:qinp.0000022725.70000.4a","journal-title":"Quantum Inf. Process."},{"key":"2_CR52","doi-asserted-by":"publisher","unstructured":"Viamontes, G.F., Markov, I.L., Hayes, J.P.: Checking equivalence of quantum circuits and states. In: 2007 IEEE\/ACM International Conference on Computer-Aided Design, pp. 69\u201374. IEEE, San Jose, CA, USA (2007). https:\/\/doi.org\/10.1109\/iccad.2007.4397246","DOI":"10.1109\/iccad.2007.4397246"},{"key":"2_CR53","doi-asserted-by":"crossref","unstructured":"Vilmart, R.: The structure of sum-over-paths, its consequences, and completeness for Clifford (2020)","DOI":"10.26226\/morressier.604907f41a80aac83ca25cb6"},{"key":"2_CR54","unstructured":"Vilmart, R.: Completeness of sum-over-paths for Toffoli-Hadamard and the dyadic fragments of quantum computation (2022)"},{"key":"2_CR55","doi-asserted-by":"publisher","unstructured":"Vilmart, R.: Rewriting and completeness of sum-over-paths in dyadic fragments of quantum computing. Logical Methods Comput. Sci. 20(1) (2024). https:\/\/doi.org\/10.46298\/lmcs-20(1:20)2024","DOI":"10.46298\/lmcs-20(1:20)2024"},{"key":"2_CR56","doi-asserted-by":"publisher","unstructured":"Vinkhuijzen, L., Grurl, T., Hillmich, S., Brand, S., Wille, R., Laarman, A.: Efficient implementation of LIMDDs for quantum circuit simulation. In: Caltais, G., Schilling, C. (eds.) Model Checking Software, pp. 3\u201321. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-32157-3_1","DOI":"10.1007\/978-3-031-32157-3_1"},{"key":"2_CR57","doi-asserted-by":"publisher","unstructured":"Watrous, J.: Quantum computational complexity. In: Meyers, R.A. (ed.) Encyclopedia of Complexity and Systems Science, pp. 7174\u20137201. Springer, New York, NY (2009). https:\/\/doi.org\/10.1007\/978-0-387-30440-3_428","DOI":"10.1007\/978-0-387-30440-3_428"},{"key":"2_CR58","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719789","volume-title":"Branching programs and binary decision diagrams: theory and applications","author":"I Wegener","year":"2000","unstructured":"Wegener, I.: Branching programs and binary decision diagrams: theory and applications. Society for Industrial and Applied Mathematics, Philadelphia, SIAM monographs on discrete mathematics and applications (2000)"},{"key":"2_CR59","unstructured":"van\u00a0de Wetering, J.: ZX-calculus for the working quantum computer scientist. arXiv:2012.13966 [quant-ph] (2020)"},{"key":"2_CR60","doi-asserted-by":"crossref","unstructured":"Wille, R., Gro\u00dfe, D., Teuber, L., Dueck, G.W., Drechsler, R.: RevLib: an online resource for reversible functions and reversible circuits. In: Int\u2019l Symp. on Multi-Valued Logic, pp. 220\u2013225 (2008)","DOI":"10.1109\/ISMVL.2008.43"},{"key":"2_CR61","doi-asserted-by":"publisher","unstructured":"Wille, R., Hillmich, S., Burgholzer, L.: Tools for quantum computing based on decision diagrams. ACM Trans. Quantum Comput. 3(3), 13:1\u201313:17 (2022). https:\/\/doi.org\/10.1145\/3491246","DOI":"10.1145\/3491246"},{"key":"2_CR62","doi-asserted-by":"crossref","unstructured":"Zulehner, A., Hillmich, S., Wille, R.: How to Efficiently Handle Complex Values? Implementing Decision Diagrams for Quantum Computing. arXiv:1911.12691 [quant-ph] (2019)","DOI":"10.1109\/ICCAD45719.2019.8942057"},{"issue":"5","key":"2_CR63","doi-asserted-by":"publisher","first-page":"848","DOI":"10.1109\/tcad.2018.2834427","volume":"38","author":"A Zulehner","year":"2019","unstructured":"Zulehner, A., Wille, R.: Advanced simulation of quantum computations. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 38(5), 848\u2013859 (2019). https:\/\/doi.org\/10.1109\/tcad.2018.2834427","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T07:39:13Z","timestamp":1784533153000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_2","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"}}]}}