{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:30:28Z","timestamp":1725539428012},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642030918"},{"type":"electronic","value":"9783642030925"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03092-5_6","type":"book-chapter","created":{"date-parts":[[2009,10,13]],"date-time":"2009-10-13T11:04:05Z","timestamp":1255431845000},"page":"56-86","source":"Crossref","is-referenced-by-count":4,"title":["Towards Model-Checking Programs with Lists"],"prefix":"10.1007","author":[{"given":"Alain","family":"Finkel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"\u00c9tienne","family":"Lozes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Sangnier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/3-540-44585-4_34","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2001","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: Trex: A tool for reachability analysis of complex systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 368\u2013372. Springer, Heidelberg (2001)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1007\/978-3-540-24730-2_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Bardin","year":"2004","unstructured":"Bardin, S., Finkel, A., Leroux, J.: FASTer acceleration of counter automata in practice. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 576\u2013590. Springer, Heidelberg (2004)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf. (to appear, 2008)","DOI":"10.1007\/s10009-008-0064-3"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11562948_35","volume-title":"Automated Technology for Verification and Analysis","author":"S. Bardin","year":"2005","unstructured":"Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 474\u2013488. Springer, Heidelberg (2005)"},{"key":"6_CR5","unstructured":"Bardin, S., Finkel, A., Lozes, \u00c9., Sangnier, A.: From pointer systems to counter systems using shape analysis. In: Proc. AVIS 2006 (2006)"},{"key":"6_CR6","unstructured":"Bardin, S., Finkel, A., Nowak, D.: Toward symbolic verification of programs handling pointers. In: Proc. AVIS 2004 (2004)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/11817963_35","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 386\u2013400. Springer, Heidelberg (2006)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/11817963_47","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 517\u2013531. Springer, Heidelberg (2006)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/978-3-540-31980-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying programs with dynamic 1-selector-linked structures in regular model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 13\u201329. Springer, Heidelberg (2005)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11823230_5","volume-title":"Static Analysis","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking of complex dynamic data structures. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 52\u201370. Springer, Heidelberg (2006)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-69738-1_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Bozga","year":"2007","unstructured":"Bozga, M., Iosif, R.: On flat programs with lists. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 122\u2013136. Springer, Heidelberg (2007)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-540-72734-7_8","volume-title":"Logical Foundations of Computer Science","author":"R. Brochenin","year":"2007","unstructured":"Brochenin, R., Demri, S., Lozes, \u00c9.: Reasoning about sequences of memory states. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol.\u00a04514, pp. 100\u2013114. Springer, Heidelberg (2007)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/11901914_36","volume-title":"Automated Technology for Verification and Analysis","author":"S. Demri","year":"2006","unstructured":"Demri, S., Finkel, A., Goranko, V., van Drimmelen, G.: Towards a model-checker for counter systems. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 493\u2013507. Springer, Heidelberg (2006)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/978-3-540-30538-5_21","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"D. Distefano","year":"2004","unstructured":"Distefano, D., Katoen, J.-P., Rensink, A.: Who is pointing when to whom? In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 250\u2013262. Springer, Heidelberg (2004)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"6_CR16","first-page":"352","volume-title":"LICS 1999","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Longo, G. (ed.) LICS 1999, pp. 352\u2013359. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"6_CR17","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)"},{"issue":"2","key":"6_CR18","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S. Ginsburg","year":"1966","unstructured":"Ginsburg, S., Spanier, E.H.: Semigroups, presburger formulas, and languages. Pacific Journal of Mathematics\u00a016(2), 285\u2013296 (1966)","journal-title":"Pacific Journal of Mathematics"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/11823230_10","volume-title":"Static Analysis","author":"L. Gonnord","year":"2006","unstructured":"Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 144\u2013160. Springer, Heidelberg (2006)"},{"key":"6_CR20","unstructured":"Homepage of LASH, \n                  \n                    http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11562948_36","volume-title":"Automated Technology for Verification and Analysis","author":"J. Leroux","year":"2005","unstructured":"Leroux, J., Sutre, G.: Flat counter automata almost everywhere! In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 489\u2013503. Springer, Heidelberg (2005)"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-45099-3_15","volume-title":"Static Analysis","author":"T. Lev-Ami","year":"2000","unstructured":"Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 280\u2013302. Springer, Heidelberg (2000)"},{"key":"6_CR23","doi-asserted-by":"publisher","first-page":"271","DOI":"10.2307\/1998219","volume":"235","author":"L. Lipshitz","year":"1978","unstructured":"Lipshitz, L.: The diophantine problem for addition and divisibility. Transactions of the American Mathematical Society\u00a0235, 271\u2013283 (1978)","journal-title":"Transactions of the American Mathematical Society"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-540-74061-2_26","volume-title":"Static Analysis","author":"S. Magill","year":"2007","unstructured":"Magill, S., Berdine, J., Clarke, E., Cook, B.: Arithmetic strengthening for shape analysis. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 419\u2013436. Springer, Heidelberg (2007)"},{"issue":"2","key":"6_CR25","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0304-3975(77)90001-9","volume":"5","author":"A. Mandel","year":"1977","unstructured":"Mandel, A., Simon, I.: On finite semigroups of matrices. Theor. Comput. Sci.\u00a05(2), 101\u2013111 (1977)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR26","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/378795.378851","volume-title":"PLDI 2001","author":"A. M\u00f8ller","year":"2001","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: PLDI 2001, pp. 221\u2013231. ACM Press, New York (2001)"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11547662_19","volume-title":"Static Analysis","author":"A. Podelski","year":"2005","unstructured":"Podelski, A., Wies, T.: Boolean heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 268\u2013283. Springer, Heidelberg (2005)"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/3-540-36575-3_15","volume-title":"Programming Languages and Systems","author":"E. Yahav","year":"2003","unstructured":"Yahav, E., Reps, T.W., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 204\u2013222. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Infinity in Logic and Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03092-5_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:04:06Z","timestamp":1619780646000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03092-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642030918","9783642030925"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03092-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}