{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:14:17Z","timestamp":1762460057546,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030945824"},{"type":"electronic","value":"9783030945831"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-94583-1_15","type":"book-chapter","created":{"date-parts":[[2022,1,13]],"date-time":"2022-01-13T22:02:34Z","timestamp":1642111354000},"page":"301-318","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["NP Satisfiability for\u00a0Arrays as\u00a0Powers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0866-9257","authenticated-orcid":false,"given":"Rodrigo","family":"Raya","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,1,14]]},"reference":[{"issue":"3","key":"15_CR1","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/s10703-017-0279-6","volume":"51","author":"F Alberti","year":"2017","unstructured":"Alberti, F., Ghilardi, S., Pagani, E.: Cardinality constraints for arrays (decidability results and applications). Formal Methods Syst. Des. 51(3), 545\u2013574 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0279-6","journal-title":"Formal Methods Syst. Des."},{"key":"15_CR2","unstructured":"Alberti, F.: An SMT-based verification framework for software systems handling arrays. Ph.D. thesis, Universit\u00e0 della Svizzera Italiana, April 2015. http:\/\/www.falberti.it\/thesis\/phd.pdf"},{"issue":"4","key":"15_CR3","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-015-9323-7","volume":"54","author":"F Alberti","year":"2015","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. J. Autom. Reason. 54(4), 327\u2013352 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9323-7","journal-title":"J. Autom. Reason."},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427\u2013442. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_28"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-319-41540-6_13","volume-title":"Computer Aided Verification","author":"P Daca","year":"2016","unstructured":"Daca, P., Henzinger, T.A., Kupriyanov, A.: Array folds logic. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 230\u2013248. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_13"},{"issue":"5","key":"15_CR6","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1016\/j.orl.2005.09.008","volume":"34","author":"F Eisenbrand","year":"2006","unstructured":"Eisenbrand, F., Shmonin, G.: Carath\u00e9odory bounds for integer cones. Oper. Res. Lett. 34(5), 564\u2013568 (2006). https:\/\/doi.org\/10.1016\/j.orl.2005.09.008","journal-title":"Oper. Res. Lett."},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Feferman, S., Vaught, R.: The first order properties of products of algebraic systems. Fundam. Math. 47(1), 57\u2013103 (1959). https:\/\/eudml.org\/doc\/213526","DOI":"10.4064\/fm-47-1-57-103"},{"key":"15_CR8","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0062837","volume-title":"The Computational Complexity of Logical Theories","author":"J Ferrante","year":"1979","unstructured":"Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718. Springer, Heidelberg (1979). https:\/\/doi.org\/10.1007\/BFb0062837"},{"issue":"1","key":"15_CR9","doi-asserted-by":"publisher","first-page":"155","DOI":"10.2307\/2042554","volume":"72","author":"J von zur Gathen","year":"1978","unstructured":"von zur Gathen, J., Sieveking, M.: A bound on solutions of linear integer equalities and inequalities. Proc. Am. Math. Soc. 72(1), 155\u2013158 (1978). https:\/\/doi.org\/10.2307\/2042554","journal-title":"Proc. Am. Math. Soc."},{"issue":"3","key":"15_CR10","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s10472-007-9078-x","volume":"50","author":"S Ghilardi","year":"2007","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell. 50(3), 231\u2013254 (2007). https:\/\/doi.org\/10.1007\/s10472-007-9078-x","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"15_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0168-0072(89)90023-7","volume":"43","author":"E Gr\u00e4del","year":"1989","unstructured":"Gr\u00e4del, E.: Dominoes and the complexity of subclasses of logical theories. Ann. Pure Appl. Logic 43(1), 1\u201330 (1989). https:\/\/doi.org\/10.1016\/0168-0072(89)90023-7","journal-title":"Ann. Pure Appl. Logic"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-78499-9_33","volume-title":"Foundations of Software Science and Computational Structures","author":"P Habermehl","year":"2008","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 474\u2013489. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78499-9_33"},{"key":"15_CR13","series-title":"Encyclopedia of Mathematics and its Applications","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574","volume-title":"Model Theory","author":"W Hodges","year":"1993","unstructured":"Hodges, W.: Model Theory. Encyclopedia of Mathematics and its Applications, Cambridge University Press, Cambridge (1993). https:\/\/doi.org\/10.1017\/CBO9780511551574"},{"issue":"3","key":"15_CR14","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10817-006-9042-1","volume":"36","author":"V Kuncak","year":"2006","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean algebra with Presburger arithmetic. J. Autom. Reason. 36(3), 213\u2013239 (2006). https:\/\/doi.org\/10.1007\/s10817-006-9042-1","journal-title":"J. Autom. Reason."},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-15205-4_5","volume-title":"Computer Science Logic","author":"V Kuncak","year":"2010","unstructured":"Kuncak, V., Piskac, R., Suter, P.: Ordered sets in the calculus of data structures. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 34\u201348. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_5"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-73595-3_15","volume-title":"Automated Deduction \u2013 CADE-21","author":"V Kuncak","year":"2007","unstructured":"Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215\u2013230. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_15"},{"key":"15_CR17","series-title":"Studies in Cognitive Systems","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-94-011-1793-7_2","volume-title":"Program Verification: Fundamental Issues in Computer Science","author":"J McCarthy","year":"1993","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds.) Program Verification: Fundamental Issues in Computer Science. Studies in Cognitive Systems, pp. 35\u201356. Springer, Dordrecht (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_2"},{"issue":"1","key":"15_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2267454","volume":"17","author":"A Mostowski","year":"1952","unstructured":"Mostowski, A.: On direct products of theories. J. Symbol. Logic 17(1), 1\u201331 (1952). https:\/\/doi.org\/10.2307\/2267454","journal-title":"J. Symbol. Logic"},{"key":"15_CR19","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bjorner, N.: Generalized, efficient array decision procedures. In: 2009 Formal Methods in Computer-Aided Design, Austin, TX, pp. 45\u201352. IEEE, November 2009. https:\/\/doi.org\/10.1109\/FMCAD.2009.5351142","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Stump, A., Barrett, C., Dill, D., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, Boston, MA, USA, pp. 29\u201337. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932480","DOI":"10.1109\/LICS.2001.932480"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-94583-1_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,14]],"date-time":"2022-01-14T00:05:44Z","timestamp":1642118744000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-94583-1_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030945824","9783030945831"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-94583-1_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"14 January 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Philadelphia, PA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 January 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl22.sigplan.org\/home\/VMCAI-2022","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":"63","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":"23","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":"0","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":"37% - 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)"}}]}}