{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:09:12Z","timestamp":1784844552037,"version":"3.55.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,3,20]],"date-time":"2015-03-20T00:00:00Z","timestamp":1426809600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10817-015-9323-7","type":"journal-article","created":{"date-parts":[[2015,3,19]],"date-time":"2015-03-19T06:45:02Z","timestamp":1426747502000},"page":"327-352","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Decision Procedures for Flat Array Properties"],"prefix":"10.1007","volume":"54","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","published-online":{"date-parts":[[2015,3,20]]},"reference":[{"key":"9323_CR1","doi-asserted-by":"crossref","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: LPAR, pp. 46\u201361 (2012)","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"9323_CR2","doi-asserted-by":"crossref","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-Based Abstraction for Arrays with Interpolants. In: CAV, pp. 679\u2013685 (2012)","DOI":"10.1007\/978-3-642-31424-7_49"},{"issue":"1","key":"9323_CR3","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s10703-014-0209-9","volume":"45","author":"F Alberti","year":"2014","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods in System Design 45(1), 63\u2013109 (2014)","journal-title":"Formal Methods in System Design"},{"key":"9323_CR4","doi-asserted-by":"crossref","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Definability of accelerated relations in a theory of arrays and its applications. In: FroCoS, pp. 23\u201339 (2013)","DOI":"10.1007\/978-3-642-40885-4_3"},{"key":"9323_CR5","doi-asserted-by":"crossref","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Booster: An acceleration-based verification framework for array programs. In: Cassez, F., Raskin, J.-F. (eds.) Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, volume 8837 of Lecture Notes in Computer Science, pp. 18\u201323, Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_2"},{"key":"9323_CR6","doi-asserted-by":"crossref","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. In: TACAS (2014)","DOI":"10.1007\/978-3-642-54862-8_2"},{"key":"9323_CR7","volume-title":"Algorithmic Number Theory. Vol. 1. Foundations of Computing Series","author":"E Bach","year":"1996","unstructured":"Bach, E., Shallit, J.: Algorithmic Number Theory. Vol. 1. Foundations of Computing Series. MIT Press (1996)"},{"key":"9323_CR8","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, pp. 171\u2013177 (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9323_CR9","unstructured":"Barrett, C., Stump A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2010)"},{"key":"9323_CR10","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL implementation secrets. In: FTRTFT, pp. 3\u201322 (2002)","DOI":"10.1007\/3-540-45739-9_1"},{"key":"9323_CR11","first-page":"373","volume-title":"TACAS, volume 8413 of Lecture Notes in Computer Science","author":"D Beyer","year":"2014","unstructured":"Beyer, D.: Status report on software verification - (competition summary sv-comp 2014). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS, volume 8413 of Lecture Notes in Computer Science, pp 373\u2013388. Springer (2014)"},{"key":"9323_CR12","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., McMillan, K.L., Rybalchenko, A.: On solving universally quantified horn clauses. In: SAS, pp. 105\u2013125 (2013)","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"9323_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem. Perspectives in Mathematical Logic","author":"E B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer-Verlag, Berlin (1997)"},{"key":"9323_CR14","volume-title":"CADE, volume 5663 of Lecture Notes in Computer Science, pp. 151\u2013156","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha, D., de Oliveira, B., D\u00e9harbe, D., Fontaine, P.: Verit: An open, trustable and efficient smt-solver. In: Schmidt, R.A. (ed.) CADE, volume 5663 of Lecture Notes in Computer Science, pp. 151\u2013156. Springer, Berlin (2009)"},{"key":"9323_CR15","doi-asserted-by":"crossref","first-page":"275","DOI":"10.3233\/FI-2009-0044","volume":"91","author":"M Bozga","year":"2009","unstructured":"Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundamenta Informaticae 91, 275\u2013303 (2009)","journal-title":"Fundamenta Informaticae"},{"key":"9323_CR16","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: VMCAI, pp. 427\u2013442 (2006)","DOI":"10.1007\/11609773_28"},{"key":"9323_CR17","doi-asserted-by":"crossref","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: CAV, vol. 1427 of LNCS, pp. 268\u2013279. Springer (1998)","DOI":"10.1007\/BFb0028751"},{"key":"9323_CR18","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9323_CR19","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":"9323_CR20","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid updates: Beyond strong vs. weak updates. In: ESOP, pp. 246\u2013266 (2010)","DOI":"10.1007\/978-3-642-11957-6_14"},{"key":"9323_CR21","unstructured":"Weber, T., Cok, D.R., Stump, A.: The 2013 SMT Evaluation. Available at http:\/\/smtcomp.sourceforge.net\/2013\/report\/SMTEVAL-2013.pdf (2013)"},{"key":"9323_CR22","doi-asserted-by":"crossref","unstructured":"Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: FSTTCS, pp. 145\u2013156 (2002)","DOI":"10.1007\/3-540-36206-1_14"},{"key":"9323_CR23","volume-title":"Shostak light. Automated deduction\u2014CADE-18, vol. 2392 of Lecture Notes in Comput. Sci., pp. 332\u2013346","author":"H Ganzinger","year":"2002","unstructured":"Ganzinger, H.: Shostak light. Automated deduction\u2014CADE-18, vol. 2392 of Lecture Notes in Comput. Sci., pp. 332\u2013346. Springer, Berlin (2002)"},{"key":"9323_CR24","doi-asserted-by":"crossref","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: CAV, pp. 306\u2013320 (2009)","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"9323_CR25","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science 6(4) (2010)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"9323_CR26","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Ranise, S.: MCMT: A Model Checker Modulo Theories. In: IJCAR, pp. 22\u201329 (2010)","DOI":"10.1007\/978-3-642-14203-1_3"},{"key":"9323_CR27","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: A logic of singly indexed arrays. In: LPAR, pp. 558\u2013573 (2008)","DOI":"10.1007\/978-3-540-89439-1_39"},{"key":"9323_CR28","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: FOSSACS (2008)","DOI":"10.1007\/978-3-540-78499-9_33"},{"issue":"2","key":"9323_CR29","doi-asserted-by":"crossref","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is ${\\varPi ^{1}_{1}}$ complete. J. Symbolic Logic 56(2), 637\u2013642 (1991)","journal-title":"J. Symbolic Logic"},{"key":"9323_CR30","doi-asserted-by":"crossref","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: TACAS, pp. 265\u2013281. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_19"},{"key":"9323_CR31","doi-asserted-by":"crossref","unstructured":"Jhala, R., McMillan, K.L.: Array Abstractions from Proofs. In: CAV (2007)","DOI":"10.1007\/978-3-540-73368-3_23"},{"key":"9323_CR32","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":"9323_CR33","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: International Federation for Information Processing Congress, pp. 21\u201328 (1962)"},{"key":"9323_CR34","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy Abstraction with Interpolants. In: CAV (2006)","DOI":"10.1007\/11817963_14"},{"key":"9323_CR35","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. In: CAV\u201905, pp. 321\u2013334 (2005)","DOI":"10.1007\/11513988_33"},{"issue":"3","key":"9323_CR36","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0022-0000(78)90021-1","volume":"16","author":"DC Oppen","year":"1978","unstructured":"Oppen, D.C.: A superexponential upper bound on the complexity of Presburger arithmetic. J. Comput. Syst. Sci. 16(3), 323\u2013332 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"9323_CR37","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krstic, S., Deters, M., Barrett, C.: Quantifier instantiation techniques for finite model finding in SMT. In: CADE, pp. 377\u2013391 (2013)","DOI":"10.1007\/978-3-642-38574-2_26"},{"key":"9323_CR38","first-page":"21","volume":"45","author":"B Rosser","year":"1938","unstructured":"Rosser, B.: The n-th prime is greater than n log n. Proc. Lond. Math. Soc., II. Ser. 45, 21\u201344 (1938)","journal-title":"Proc. Lond. Math. Soc., II. Ser."},{"key":"9323_CR39","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1070\/IM1984v022n03ABEH001456","volume":"22","author":"AL Sem\u00ebnov","year":"1984","unstructured":"Sem\u00ebnov, A.L.: Logical theories of one-place functions on the set of natural numbers. Izvestiya: Mathematics 22, 587\u2013618 (1984)","journal-title":"Izvestiya: Mathematics"},{"key":"9323_CR40","unstructured":"Shoenfield, J.R.: Mathematical logic. Association for Symbolic Logic, Urbana, IL. Reprint of the 1973 second printing (2001)"},{"issue":"3","key":"9323_CR41","doi-asserted-by":"crossref","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. 34(3), 209\u2013238 (2005)","journal-title":"J. Automat. Reason."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9323-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9323-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9323-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T00:50:53Z","timestamp":1598835053000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9323-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,20]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["9323"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9323-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,20]]}}}