{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:39Z","timestamp":1776305379490,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031384981","type":"print"},{"value":"9783031384998","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a theory of Cartesian arrays, which are multi-dimensional arrays with support for the projection of arrays to sub-arrays, as well as for updating sub-arrays. The resulting logic is an extension of Combinatorial Array Logic (CAL) and is motivated by the analysis of quantum circuits: using projection, we can succinctly encode the semantics of quantum gates as quantifier-free formulas and verify the end-to-end correctness of quantum circuits. Since the logic is expressive enough to represent quantum circuits succinctly, it necessarily has a high complexity; as we show, it suffices to encode the<jats:italic>k<\/jats:italic>-color problem of a graph under a succinct circuit representation, an NEXPTIME-complete problem. We present an NEXPTIME decision procedure for the logic and report on preliminary experiments with the analysis of quantum circuits using this decision procedure.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_10","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"170-189","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["A Theory of\u00a0Cartesian Arrays (with Applications in\u00a0Quantum Circuit Verification)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-0336","authenticated-orcid":false,"given":"Yu-Fang","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2733-7098","authenticated-orcid":false,"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wei-Lun","family":"Tsai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Amy, M.: Towards large-scale functional verification of universal quantum circuits. In: Quantum Physics and Logic (2018)","DOI":"10.4204\/EPTCS.287.1"},{"key":"10_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-031-27481-7_12","volume-title":"Formal Methods","author":"F Bauer-Marquart","year":"2023","unstructured":"Bauer-Marquart, F., Leue, S., Schilling, C.: symqv: automated symbolic verification of quantum programs. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 181\u2013198. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_12"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Bernstein, E., Vazirani, U.V.: Quantum complexity theory. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16\u201318, 1993, San Diego, CA, USA, pp. 11\u201320. ACM (1993). https:\/\/doi.org\/10.1145\/167088.167097","DOI":"10.1145\/167088.167097"},{"key":"10_CR5","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: CDSAT for nondisjoint theories with shared predicates: arrays with abstract length. In: D\u00e9harbe, D., Hyv\u00e4rinen, A.E.J. (eds.) Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories Co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) Part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, 11\u201312 August 2022. CEUR Workshop Proceedings, vol. 3185, pp. 18\u201337. CEUR-WS.org (2022). https:\/\/ceur-ws.org\/Vol-3185\/paper9712.pdf"},{"issue":"1\u20133","key":"10_CR6","doi-asserted-by":"publisher","first-page":"165","DOI":"10.3233\/sat190067","volume":"6","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. J. Satisf. Boolean Model. Comput. 6(1\u20133), 165\u2013201 (2009). https:\/\/doi.org\/10.3233\/sat190067","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Chen, Y., Chung, K., Leng\u00e1l, O., Lin, J., Tsai, W., Yen, D.: An automata-based framework for verification and bug hunting in quantum circuits (2023). https:\/\/doi.org\/10.48550\/arxiv.2301.07747, https:\/\/arxiv.org\/abs\/2301.07747. To appear at PLDI 2023","DOI":"10.48550\/arxiv.2301.07747"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-319-24246-0_8","volume-title":"Frontiers of Combining Systems","author":"J Christ","year":"2015","unstructured":"Christ, J., Hoenicke, J.: Weakly equivalent arrays. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 119\u2013134. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_8"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New J. Phys. 13(4), 043016 (2011). https:\/\/doi.org\/10.1088\/1367-2630\/13\/4\/043016","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"10_CR10","unstructured":"Dawson, C.M., Nielsen, M.A.: The Solovay-Kitaev algorithm. arXiv preprint quant-ph\/0505030 (2005)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: 2009 Formal Methods in Computer-Aided Design, pp. 45\u201352. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-54108-7_6","volume-title":"Verified Software: Theories, Tools, Experiments","author":"S Falke","year":"2014","unstructured":"Falke, S., Merz, F., Sinz, C.: Extending the theory of arrays: memset, memcpy, and beyond. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 108\u2013128. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_6"},{"issue":"7","key":"10_CR13","doi-asserted-by":"publisher","first-page":"1181","DOI":"10.1016\/j.jcss.2013.04.002","volume":"79","author":"Y Feng","year":"2013","unstructured":"Feng, Y., Yu, N., Ying, M.: Model checking quantum Markov chains. J. Comput. Syst. Sci. 79(7), 1181\u20131198 (2013). https:\/\/doi.org\/10.1016\/j.jcss.2013.04.002","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"MC Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, New York (1996). https:\/\/doi.org\/10.1007\/978-1-4612-2360-3","edition":"2"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519\u2013531. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_52"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519\u2013531. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_52"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Grover, L.K.: A fast quantum mechanical algorithm for database search. In: Miller, G.L. (ed.) Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA, 22\u201324 May 1996, pp. 212\u2013219. ACM (1996). https:\/\/doi.org\/10.1145\/237814.237866","DOI":"10.1145\/237814.237866"},{"key":"10_CR18","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)"},{"key":"10_CR19","unstructured":"Hietala, K., Rand, R., Hung, S.H., Wu, X., Hicks, M.: Verified optimization in a quantum intermediate representation. arXiv preprint arXiv:1904.06319 (2019)"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-030-11245-5_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Hoenicke","year":"2019","unstructured":"Hoenicke, J., Schindler, T.: Solving and interpolating constant arrays based on weak equivalences. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 297\u2013317. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_14"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Mateus, P., Ramos, J., Sernadas, A., Sernadas, C.: Temporal Logics for Reasoning about Quantum Systems, pp. 389\u2013413. Cambridge University Press, Cambridge (2009). https:\/\/doi.org\/10.1017\/CBO9781139193313.011","DOI":"10.1017\/CBO9781139193313.011"},{"key":"10_CR22","volume-title":"Quantum Computation and Quantum Information: 10th Anniversary Edition","author":"MA Nielsen","year":"2011","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information: 10th Anniversary Edition, 10th edn. Cambridge University Press, USA (2011)","edition":"10"},{"issue":"3","key":"10_CR23","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/S0019-9958(86)80009-2","volume":"71","author":"CH Papadimitriou","year":"1986","unstructured":"Papadimitriou, C.H., Yannakakis, M.: A note on succinct representations of graphs. Inf. Control 71(3), 181\u2013185 (1986)","journal-title":"Inf. Control"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-540-69166-2_18","volume-title":"Static Analysis","author":"S Perdrix","year":"2008","unstructured":"Perdrix, S.: Quantum entanglement analysis based on abstract interpretation. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 270\u2013282. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69166-2_18"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-030-94583-1_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Raya","year":"2022","unstructured":"Raya, R., Kun\u010dak, V.: NP satisfiability for\u00a0arrays as\u00a0powers. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 301\u2013318. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_15"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-031-10769-6_9","volume-title":"Automated Reasoning","author":"Y Sheng","year":"2022","unstructured":"Sheng, Y., et al.: Reasoning about vectors using an SMT theory of sequences. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 125\u2013143. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_9"},{"issue":"1","key":"10_CR28","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/230514.571645","volume":"27","author":"M Sipser","year":"1996","unstructured":"Sipser, M.: Introduction to the theory of computation. ACM SIGACT News 27(1), 27\u201329 (1996)","journal-title":"ACM SIGACT News"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp. 29\u201337. IEEE (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"Tsai, Y., Jiang, J.R., Jhang, C.: Bit-slicing the Hilbert space: scaling up accurate quantum circuit simulation. In: 58th ACM\/IEEE Design Automation Conference, DAC 2021, San Francisco, CA, USA, 5\u20139 December 2021, pp. 439\u2013444. IEEE (2021). https:\/\/doi.org\/10.1109\/DAC18074.2021.9586191","DOI":"10.1109\/DAC18074.2021.9586191"},{"key":"10_CR31","doi-asserted-by":"publisher","unstructured":"Wang, Q., Appel, A.W.: A solver for arrays with concatenation. J. Autom. Reason. 67(1), 4 (2023). https:\/\/doi.org\/10.1007\/s10817-022-09654-y","DOI":"10.1007\/s10817-022-09654-y"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Xu, M., Fu, J., Mei, J., Deng, Y.: Model checking QCTL plus on quantum Markov chains. Theor. Comput. Sci. 913, 43\u201372 (2022). https:\/\/doi.org\/10.1016\/j.tcs.2022.01.044","DOI":"10.1016\/j.tcs.2022.01.044"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Xu, M., et al.: Quartz: superoptimization of quantum circuits. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 625\u2013640 (2022)","DOI":"10.1145\/3519939.3523433"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 542\u2013558 (2021)","DOI":"10.1145\/3453483.3454061"},{"key":"10_CR35","doi-asserted-by":"publisher","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","DOI":"10.1109\/TCAD.2018.2834427"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T10:35:25Z","timestamp":1730025325000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}