{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T13:25:55Z","timestamp":1758633955549,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642156427"},{"type":"electronic","value":"9783642156434"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15643-4_11","type":"book-chapter","created":{"date-parts":[[2010,9,20]],"date-time":"2010-09-20T09:39:39Z","timestamp":1284975579000},"page":"128-142","source":"Crossref","is-referenced-by-count":7,"title":["What\u2019s Decidable about Sequences?"],"prefix":"10.1007","author":[{"given":"Carlo A.","family":"Furia","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"11_CR1","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1016\/S0747-7171(89)80056-2","volume":"8","author":"H. Abdulrab","year":"1989","unstructured":"Abdulrab, H., P\u00e9cuchet, J.P.: Solving word equations. Journal of Symbolic Computation\u00a08(5), 499\u2013521 (1989)","journal-title":"Journal of Symbolic Computation"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/978-3-642-02658-4_15","volume-title":"CAV 2009","author":"M. Bozga","year":"2009","unstructured":"Bozga, M., Habermehl, P., Iosif, R., Konecn\u00fd, F., Vojnar, T.: Automatic verification of integer array programs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 157\u2013172. Springer, Heidelberg (2009)"},{"key":"11_CR3","volume-title":"The Calculus of Computation","author":"A.R. Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation. Springer, Heidelberg (2007)"},{"key":"11_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":"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":"11_CR5","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1002\/malq.19880340410","volume":"34","author":"J.R. B\u00fcchi","year":"1988","unstructured":"B\u00fcchi, J.R., Senger, S.: Definability in the existential theory of concatenation and undecidable extensions of this theory. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik\u00a034, 337\u2013342 (1988)","journal-title":"Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Proceedings of 9th Conference on Formal Methods in Computer Aided Design (FMCAD 2009), pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"11_CR7","volume-title":"Algebraic Combinatorics on Words","author":"V. Diekert","year":"2002","unstructured":"Diekert, V.: Makanin\u2019s algorithm. In: Lothaire, M. (ed.) Algebraic Combinatorics on Words. Cambridge University Press, Cambridge (2002)"},{"issue":"5","key":"11_CR8","first-page":"1067","volume":"36","author":"V.G. Durnev","year":"1995","unstructured":"Durnev, V.G.: Unsolvability of the positive \u2200\u2009\u2203\u20093-theory of a free semi-group. Sibirski\u012d Matematicheski\u012d Zhurnal\u00a036(5), 1067\u20131080 (1995)","journal-title":"Sibirski\u012d Matematicheski\u012d Zhurnal"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Furia, C.A.: What\u2019s decidable about sequences? (January 2010), \n                    \n                      http:\/\/arxiv.org\/abs\/1001.2100","DOI":"10.1007\/978-3-642-15643-4_11"},{"issue":"3-4","key":"11_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. Annals of Mathematics and Artificial Intelligence\u00a050(3-4), 231\u2013254 (2007)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"11_CR11","series-title":"Lecture Notes in Artificial Intelligence","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":"11_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.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 474\u2013489. Springer, Heidelberg (2008)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-11319-2_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. Kuncak","year":"2010","unstructured":"Kuncak, V., Piskac, R., Suter, P., Wies, T.: Building a calculus of data structures. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 26\u201344. Springer, Heidelberg (2010)"},{"issue":"2","key":"11_CR14","first-page":"147","volume":"103","author":"G.S. Makanin","year":"1977","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. Rossi\u012dskaya Akademiya Nauk. Matematicheski\u012d Sbornik (Translated in Sbornik Mathematics)\u00a0103(2), 147\u2013236 (1977)","journal-title":"Matematicheski\u012d Sbornik (Translated in Sbornik Mathematics)"},{"key":"11_CR15","volume-title":"Object-oriented software construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-oriented software construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-78163-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 218\u2013232. Springer, Heidelberg (2008)"},{"issue":"3","key":"11_CR17","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1145\/990308.990312","volume":"51","author":"W. Plandowski","year":"2004","unstructured":"Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. Journal of the ACM\u00a051(3), 483\u2013496 (2004)","journal-title":"Journal of the ACM"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/BFb0023779","volume-title":"Computer Science Logic","author":"S. Seibert","year":"1992","unstructured":"Seibert, S.: Quantifier hierarchies over word relations. In: Kleine B\u00fcning, H., J\u00e4ger, G., B\u00f6rger, E., Richter, M.M. (eds.) CSL 1991. LNCS, vol.\u00a0626, pp. 329\u2013352. Springer, Heidelberg (1992)"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1145\/1375581.1375624","volume-title":"Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008)","author":"K. Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI 2008), pp. 349\u2013361. ACM, New York (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15643-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T18:57:27Z","timestamp":1558292247000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15643-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642156427","9783642156434"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15643-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}