{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,12]],"date-time":"2026-09-12T11:01:40Z","timestamp":1789210900043,"version":"build-2803163510"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642548611","type":"print"},{"value":"9783642548628","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54862-8_2","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T13:33:34Z","timestamp":1395408814000},"page":"15-30","source":"Crossref","is-referenced-by-count":17,"title":["Decision Procedures for Flat Array Properties"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Alberti","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-28717-6_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F. Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18. LNCS, vol.\u00a07180, pp. 46\u201361. Springer, Heidelberg (2012)"},{"key":"2_CR2","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. Technical Report 2013\/04, University of Lugano (October 2013), http:\/\/www.inf.usi.ch\/research_publication.htm?id=77"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-40885-4_3","volume-title":"Frontiers of Combining Systems","author":"F. Alberti","year":"2013","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Definability of accelerated relations in a theory of arrays and its applications. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol.\u00a08152, pp. 23\u201339. Springer, Heidelberg (2013)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-45739-9_1","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"G. Behrmann","year":"2002","unstructured":"Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL implementation secrets. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol.\u00a02469, pp. 3\u201322. Springer, Heidelberg (2002)"},{"key":"2_CR6","series-title":"Perspectives in Mathematical Logic","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The classical decision problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The classical decision problem. Perspectives in Mathematical Logic. Springer, Berlin (1997)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundamenta Informaticae\u00a0(91), 275\u2013303 (2009)","DOI":"10.3233\/FI-2009-0044"},{"key":"2_CR8","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":"A.R. Bradley","year":"2006","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.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2006)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 268\u2013279. Springer, Heidelberg (1998)"},{"key":"2_CR10","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. Moura de","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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"2_CR11","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-36206-1_14","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"A. Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol.\u00a02556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"key":"2_CR13","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/3-540-45620-1_28","volume-title":"Automated Deduction - CADE-18","author":"H. Ganzinger","year":"2002","unstructured":"Ganzinger, H.: Shostak light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 332\u2013346. Springer, Heidelberg (2002)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"2_CR15","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1007\/978-3-540-89439-1_39","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Habermehl","year":"2008","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: A logic of singly indexed arrays. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 558\u2013573. Springer, Heidelberg (2008)"},{"key":"2_CR16","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.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 474\u2013489. Springer, Heidelberg (2008)"},{"issue":"2","key":"2_CR17","doi-asserted-by":"publisher","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"J.Y. Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is $\\Pi^1_1$ complete. J. Symbolic Logic\u00a056(2), 637\u2013642 (1991), doi:10.2307\/2274706","journal-title":"J. Symbolic Logic"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Lewis, H.B.: Complexity of solvable cases of the decision problem for the predicate calculus. In: 19th Ann. Symp. on Found. of Comp. Sci. pp. 35\u201347. IEEE (1978)","DOI":"10.1109\/SFCS.1978.9"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 321\u2013334. Springer, Heidelberg (2005)"},{"issue":"3","key":"2_CR21","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(78)90021-1","volume":"16","author":"D.C. Oppen","year":"1978","unstructured":"Oppen, D.C.: A superexponential upper bound on the complexity of Presburger arithmetic. J. Comput. System Sci.\u00a016(3), 323\u2013332 (1978)","journal-title":"J. Comput. System Sci."},{"key":"2_CR22","unstructured":"Ranise, S., Tinelli, C.: The Satisfiability Modulo Theories Library, SMT-LIB (2006), http:\/\/www.smt-lib.org"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-38574-2_26","volume-title":"Automated Deduction \u2013 CADE-24","author":"A. Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 377\u2013391. Springer, Heidelberg (2013)"},{"key":"2_CR24","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1070\/IM1984v022n03ABEH001456","volume":"22","author":"A.L. Sem\u00ebnov","year":"1984","unstructured":"Sem\u00ebnov, A.L.: Logical theories of one-place functions on the set of natural numbers. Izvestiya: Mathematics\u00a022, 587\u2013618 (1984)","journal-title":"Izvestiya: Mathematics"},{"key":"2_CR25","unstructured":"Shoenfield, J.R.: Mathematical logic. Association for Symbolic Logic, Urbana (2001) (reprint of the 1973 second printing )"},{"issue":"3","key":"2_CR26","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C. Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Automat. Reason.\u00a034(3), 209\u2013238 (2005)","journal-title":"J. Automat. Reason."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54862-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,16]],"date-time":"2020-08-16T16:34:54Z","timestamp":1597595694000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54862-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548611","9783642548628"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54862-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}