{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:44Z","timestamp":1763468024673},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T00:00:00Z","timestamp":1295308800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2011,4]]},"DOI":"10.1007\/s10703-011-0111-7","type":"journal-article","created":{"date-parts":[[2011,1,17]],"date-time":"2011-01-17T18:18:18Z","timestamp":1295288298000},"page":"158-192","source":"Crossref","is-referenced-by-count":20,"title":["Programs with lists are counter automata"],"prefix":"10.1007","volume":"38","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Habermehl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Moro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,1,18]]},"reference":[{"key":"111_CR1","series-title":"LNCS","volume-title":"Proc of CAV\u201908","author":"PA Abdulla","year":"2008","unstructured":"Abdulla PA, Bouajjani A, Cederberg J, Haziza F, Rezine A (2008) Monotonic abstraction for programs with dynamic memory heaps. In: Proc of CAV\u201908. LNCS, vol\u00a05123. Springer, Berlin"},{"key":"111_CR2","series-title":"LNCS","volume-title":"Proc of CAV\u201901","author":"A Annichini","year":"2001","unstructured":"Annichini A, Bouajjani A, Sighireanu M (2001) TReX: A tool for reachability analysis of complex systems. In: Proc of CAV\u201901. LNCS, vol\u00a02102"},{"key":"111_CR3","series-title":"LNCS","volume-title":"Proc of VMCAI\u201905","author":"I Balaban","year":"2005","unstructured":"Balaban I, Pnueli A, Zuck LD (2005) Shape analysis by predicate abstraction. In: Proc of VMCAI\u201905. LNCS, vol 3385. Springer, Berlin"},{"key":"111_CR4","unstructured":"Baldan P, Corradini A, Esparza J, Heindel T, K\u00f6nig B, Kozioura V (2005) Verifying red-black trees. In: Proc of COSMICAH\u201905, Technical report RR-05-04. Queen Mary, University of London"},{"key":"111_CR5","volume-title":"Proc of AVIS\u201904","author":"S Bardin","year":"2004","unstructured":"Bardin S, Finkel A, Nowak D (2004) Toward symbolic verification of programs handling pointers. In: Proc of AVIS\u201904"},{"key":"111_CR6","series-title":"LNCS","volume-title":"Proc of CAV\u201903","author":"S Bardin","year":"2003","unstructured":"Bardin S, Finkel A, Leroux J, Petrucci L (2003) FAST: Fast acceleration of symbolic transition systems. In: Proc of CAV\u201903. LNCS, vol\u00a02725"},{"key":"111_CR7","volume-title":"Proc of AVIS\u201906","author":"S Bardin","year":"2006","unstructured":"Bardin S, Finkel A, Lozes E (2006) From pointer systems to counter systems using shape analysis. In: Proc of AVIS\u201906"},{"key":"111_CR8","series-title":"LNCS","volume-title":"Proc of CAV\u201907","author":"J Berdine","year":"2007","unstructured":"Berdine J, Calcagno C, Cook B, Distefano D, O\u2019Hearn PW, Wies T, Yang H (2007) Shape analysis for composite data structures. In: Proc of CAV\u201907. LNCS, vol\u00a04590. Springer, Berlin"},{"key":"111_CR9","volume-title":"Proc of POPL\u201907","author":"J Berdine","year":"2007","unstructured":"Berdine J, Chawdhary A, Cook B, Distefano D, O\u2019Hearn PW (2007) Variance analyses from invariance analyses. In: Proc of POPL\u201907. ACM Press, New York"},{"key":"111_CR10","series-title":"LNCS","volume-title":"Proc of CAV\u201906","author":"A Bouajjani","year":"2006","unstructured":"Bouajjani A, Bozga M, Habermehl P, Iosif R, Moro P, Vojnar T (2006) Programs with lists are counter automata. In: Proc of CAV\u201906. LNCS, vol\u00a04144. Springer, Berlin"},{"key":"111_CR11","series-title":"LNCS","volume-title":"Proc of TACAS\u201905","author":"A Bouajjani","year":"2005","unstructured":"Bouajjani A, Habermehl P, Moro P, Vojnar T (2005) Verifying programs with dynamic 1-selector-linked structures in regular model checking. In: Proc of TACAS\u201905. LNCS, vol\u00a03440. Springer, Berlin"},{"key":"111_CR12","series-title":"LNCS","volume-title":"Proc of SAS\u201906","author":"A Bouajjani","year":"2006","unstructured":"Bouajjani A, Habermehl P, Rogalewicz A, Vojnar T (2006) Abstract regular tree model checking of complex dynamic data structures. In: Proc of SAS\u201906. LNCS, vol\u00a04134. Springer, Berlin"},{"key":"111_CR13","volume-title":"Proc of VISSAS\u201905","author":"M Bozga","year":"2005","unstructured":"Bozga M, Iosif R (2005) Quantitative verification of programs with lists. In: Proc of VISSAS\u201905"},{"key":"111_CR14","volume-title":"Proc of PEPM\u201903","author":"M Bozga","year":"2003","unstructured":"Bozga M, Iosif R, Lakhnech Y (2003) Storeless semantics and alias logic. In: Proc of PEPM\u201903. ACM Press, New York"},{"key":"111_CR15","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-540-69738-1_9","volume-title":"VMCAI\u201907: Proceedings of the 8th international conference on verification, model checking, and abstract interpretation","author":"M Bozga","year":"2007","unstructured":"Bozga M, Iosif R (2007) On flat programs with lists. In: VMCAI\u201907: Proceedings of the 8th international conference on verification, model checking, and abstract interpretation. Springer, Berlin, pp\u00a0122\u2013136"},{"key":"111_CR16","series-title":"LNCS","volume-title":"Proc of CONCUR\u201905","author":"A Bradley","year":"2005","unstructured":"Bradley A, Manna Z, Sipma H (2005) Termination analysis of integer linear loops. In: Proc of CONCUR\u201905. LNCS, vol\u00a03653"},{"key":"111_CR17","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/j.entcs.2005.10.008","volume":"145","author":"M \u010ce\u0161ka","year":"2006","unstructured":"\u010ce\u0161ka M, Erlebach P, Vojnar T (2006) Pattern-based verification of programs with extended linear linked data structures. Electron Notes Theor Comput Sci 145:113\u2013130","journal-title":"Electron Notes Theor Comput Sci"},{"key":"111_CR18","series-title":"LNCS","volume-title":"Proc of SAS\u201905","author":"B Cook","year":"2005","unstructured":"Cook B, Podelski A, Rybalchenko A (2005) Abstraction refinement for termination. In: Proc of SAS\u201905. LNCS, vol\u00a03672. Springer, Berlin"},{"key":"111_CR19","series-title":"LNCS","volume-title":"Proc of TACAS\u201906","author":"JV Deshmukh","year":"2006","unstructured":"Deshmukh JV, Emerson EA, Gupta P (2006) Automatic verification of parameterized data structures. In: Proc of TACAS\u201906. LNCS, vol\u00a03920. Springer, Berlin"},{"key":"111_CR20","series-title":"LNCS","volume-title":"Proc of CAV\u201906","author":"D Distefano","year":"2006","unstructured":"Distefano D, Berdine J, Cook B, O\u2019Hearn PW (2006) Automatic termination proofs for programs with shape-shifting heaps. In: Proc of CAV\u201906. LNCS, vol\u00a04144. Springer, Berlin"},{"key":"111_CR21","series-title":"LNCS","volume-title":"Proc of TACAS\u201906","author":"D Distefano","year":"2006","unstructured":"Distefano D, O\u2019Hearn PW, Yang H (2006) A local shape analysis based on separation logic. In: Proc of TACAS\u201906. LNCS, vol\u00a03920. Springer, Berlin"},{"key":"111_CR22","unstructured":"Habermehl P, Iosif R, Rogalewicz A, Vojnar T (2007) Proving termination of tree manipulating programs. Technical Report TR-2007-1, Verimag"},{"key":"111_CR23","first-page":"302","volume-title":"STTT","author":"R Iosif","year":"2004","unstructured":"Iosif R (2004) Symmetry reductions for model checking of concurrent dynamic software. In: STTT, pp\u00a0302\u2013319"},{"key":"111_CR24","unstructured":"Iosif R, Bozga M, Konecny F Flata. http:\/\/www-verimag.imag.fr\/FLATA.html"},{"key":"111_CR25","unstructured":"Iosif R, Bozga M, Perarnau S L2CA: Lists to counter automata. http:\/\/www-verimag.imag.fr\/L2CA-homepage.html"},{"key":"111_CR26","unstructured":"The LASH toolset. http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"111_CR27","series-title":"LNCS","volume-title":"Proc of ESOP\u201905","author":"O Lee","year":"2005","unstructured":"Lee O, Yang H, Yi K (2005) Automatic verification of pointer programs using grammar-based shape analysis. In: Proc of ESOP\u201905. LNCS, vol\u00a03444. Springer, Berlin"},{"key":"111_CR28","series-title":"LNCS","volume-title":"Proc of SAS\u201906","author":"A Loginov","year":"2006","unstructured":"Loginov A, Reps TW, Sagiv M (2006) Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: Proc of SAS\u201906. LNCS, vol\u00a04134. Springer, Berlin"},{"key":"111_CR29","series-title":"LNCS","volume-title":"Proc of VMCAI\u201905","author":"R Manevich","year":"2005","unstructured":"Manevich R, Yahav E, Ramalingam G, Sagiv M (2005) Predicate abstraction and canonical abstraction for singly-linked lists. In: Proc of VMCAI\u201905. LNCS, vol\u00a03385. Springer, Berlin"},{"key":"111_CR30","volume-title":"Proc of PLDI\u201901","author":"A M\u00f8ller","year":"2001","unstructured":"M\u00f8ller A, Schwartzbach MI (2001) The pointer assertion logic engine. In: Proc of PLDI\u201901. ACM Press, New York"},{"key":"111_CR31","volume-title":"Proc. of LICS\u201902","author":"JC Reynolds","year":"2002","unstructured":"Reynolds JC (2002) Separation logic: A logic for shared mutable data structures. In: Proc. of LICS\u201902. IEEE CS Press, Los Alamitos"},{"key":"111_CR32","unstructured":"Rybalchenko A ARMC: Abstraction refinement model checker. http:\/\/www7.in.tum.de\/rybal\/armc\/"},{"key":"111_CR33","doi-asserted-by":"crossref","unstructured":"Sagiv S, Reps TW, Wilhelm R (2002) Parametric shape analysis via 3-valued logic. ACM Trans Program Lang Syst 24(3)","DOI":"10.1145\/514188.514190"},{"key":"111_CR34","series-title":"LNCS","volume-title":"Proc of ESOP\u201903","author":"E Yahav","year":"2003","unstructured":"Yahav E, Reps T, Sagiv M, Wilhelm R (2003) Verifying temporal heap properties specified via evolution logic. In: Proc of ESOP\u201903. LNCS, vol\u00a02618. Springer, Berlin"},{"key":"111_CR35","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1145\/1394622","volume-title":"Proc of CAV\u201908","author":"H Yang","year":"2008","unstructured":"Yang H, Lee O, Berdine J, Calcagno C, Cook B, Distefano D, O\u2019Hearn PW (2008) Scalable shape analysis for systems code. In: Proc of CAV\u201908. LNCS, vol\u00a05123. Springer, Berlin"},{"key":"111_CR36","series-title":"LNCS","volume-title":"Proc of SAS\u201902","author":"T Yavuz-Kahveci","year":"2002","unstructured":"Yavuz-Kahveci T, Bultan T (2002) Automated verification of concurrent linked lists with counters. In: Proc of SAS\u201902. LNCS, vol\u00a02477. Springer, Berlin"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0111-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0111-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0111-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T22:49:11Z","timestamp":1559947751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0111-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,18]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,4]]}},"alternative-id":["111"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0111-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1,18]]}}}