{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:00:15Z","timestamp":1725494415378},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_9","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T07:58:07Z","timestamp":1194854287000},"page":"122-136","source":"Crossref","is-referenced-by-count":3,"title":["On Flat Programs with Lists"],"prefix":"10.1007","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","first-page":"17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.: Shape Analysis by Predicate Abstraction. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 17\u201319. Springer, Heidelberg (2005)"},{"key":"9_CR2","unstructured":"Bardin, S., Finkel, A., Nowak, D.: Toward Symbolic Verification of Programs Handling Pointers. AVIS. Barcelona, Spain (2004)"},{"key":"9_CR3","unstructured":"Bardin, S., Finkel, A., Lozes, E., Sangnier, A.: From pointer systems to counter systems using shape analysis. In: 5th International Workshop on Automated Verification of Infinite-State Systems, AVIS (2006)"},{"key":"9_CR4","first-page":"15","volume":"60","author":"A.P. Beltyukov","year":"1976","unstructured":"Beltyukov, A.P.: Decidability of the universal theory of natural numbers with addition and divisibility. Zapiski Nauch. Sem. Leningrad Otdeleniya Mathematical Institute\u00a060, 15\u201328 (1976)","journal-title":"Zapiski Nauch. Sem. Leningrad Otdeleniya Mathematical Institute"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.: A Decidable Fragment of Separation Logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, Springer, Heidelberg (2004)"},{"key":"9_CR6","unstructured":"B\u00e9s, A.: A survey of arithmetical definability. A Tribute to Maurice Boffa. Bulletin de la Soci\u00e9t\u00e9 Math\u00e9matique de Belgique, 1\u201354 (2002)"},{"issue":"2","key":"9_CR7","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1016\/S0304-3975(03)00314-1","volume":"309","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B.: On iterating linear transformations over recognizable sets of integers. TCS\u00a0309(2), 413\u2013468 (2003)","journal-title":"TCS"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., et al.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, Springer, Heidelberg (2006)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. Technical Report TR-2006-3, VERIMAG (2006)","DOI":"10.1007\/11817963_47"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., et al.: Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, Springer, Heidelberg (2005)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-3-540-31982-5_27","volume-title":"Foundations of Software Science and Computational Structures","author":"M. Bozga","year":"2005","unstructured":"Bozga, M., Iosif, R.: On decidability within the arithmetic of addition and divisibility. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 425\u2013439. Springer, Heidelberg (2005)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Chakaravarthy, V.T.: New results on the computability and complexity of points-to-analysis. In: International Conference on Principles of Programming Languages, POPL (2003)","DOI":"10.1145\/604131.604142"},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/2371045","volume":"58","author":"A. Church","year":"1936","unstructured":"Church, A.: An unsolvable problem of elementary number theory. American Journal of Mathematics\u00a058, 345\u2013363 (1936)","journal-title":"American Journal of Mathematics"},{"key":"9_CR14","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":"9_CR15","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.) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a02556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K. G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik\u00a038, 173\u2013198 (1931)","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: POPL (2001)","DOI":"10.1145\/360204.375719"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"271","DOI":"10.2307\/1998219","volume":"235","author":"L. Lipshitz","year":"1976","unstructured":"Lipshitz, L.: The diophantine problem for addition and divisibility. Transaction of the American Mathematical Society\u00a0235, 271\u2013283 (1976)","journal-title":"Transaction of the American Mathematical Society"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Manevich","year":"2005","unstructured":"Manevich, R., et al.: Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, Springer, Heidelberg (2005)"},{"key":"9_CR20","first-page":"354","volume":"11","author":"Y. Matiyasevich","year":"1970","unstructured":"Matiyasevich, Y.: Enumerable sets are diophantine. Journal of Sovietic Mathematics\u00a011, 354\u2013358 (1970)","journal-title":"Journal of Sovietic Mathematics"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The Pointer Assertion Logic Engine. In: PLDI (2001)","DOI":"10.1145\/378795.378851"},{"key":"9_CR22","unstructured":"Presburger, M.: \u00dcber die Vollstandigkeit eines gewissen Systems der Arithmetik. In: Comptes rendus du I Congr\u00e9s des Pays Slaves, Warsaw (1929)"},{"issue":"2","key":"9_CR23","doi-asserted-by":"publisher","first-page":"98","DOI":"10.2307\/2266510","volume":"14","author":"J. Robinson","year":"1949","unstructured":"Robinson, J.: Definability and decision problems in arithmetic. The Journal of Symbolic Logic\u00a014(2), 98\u2013114 (1949)","journal-title":"The Journal of Symbolic Logic"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic. In: TOPLAS (2002)","DOI":"10.1145\/514188.514190"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:45:12Z","timestamp":1620002712000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_9","relation":{},"subject":[]}}