{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T18:24:39Z","timestamp":1694629479801},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2007,8,1]],"date-time":"2007-08-01T00:00:00Z","timestamp":1185926400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2007,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The paper deals with the problem of automatic verification of programs working with extended linear linked dynamic data structures, in particular, pattern-based verification is considered. In this approach, one can abstract memory configurations by abstracting away the exact number of adjacent occurrences of certain memory patterns. With respect to the previous work on the subject the method presented in the paper has been extended to be able to handle multiple patterns, which allows for verification of programs working with more types of structures and\/or with structures with irregular shapes. The experimental results obtained from a prototype implementation of the method show that the method is very competitive and offers a big potential for future extensions.<\/jats:p>","DOI":"10.1007\/s00165-007-0031-x","type":"journal-article","created":{"date-parts":[[2007,3,29]],"date-time":"2007-03-29T17:23:46Z","timestamp":1175189026000},"page":"363-374","source":"Crossref","is-referenced-by-count":2,"title":["Generalised multi-pattern-based verification of programs with linear linked structures"],"prefix":"10.1145","volume":"19","author":[{"given":"Milan","family":"\u010ce\u0161ka","sequence":"first","affiliation":[{"name":"FIT, Brno University of Technology, Bo\u017eet\u011bchova 2, 61266, Brno, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavel","family":"Erlebach","sequence":"additional","affiliation":[{"name":"FIT, Brno University of Technology, Bo\u017eet\u011bchova 2, 61266, Brno, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[{"name":"FIT, Brno University of Technology, Bo\u017eet\u011bchova 2, 61266, Brno, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Bouajjani A Habermehl P Moro P Vojnar T (2005) Verifying programs with dynamic 1-selector-linked structures in regular model checking. In: Proceedings of TACAS\u201905. LNCS Vol 3440. Springer Heidelberg","DOI":"10.1007\/978-3-540-31980-1_2"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bouajjani A Habermehl P Vojnar T (2004) Abstract regular model checking. In: Proceedings of CAV\u201904. LNCS Vol 3114. Springer Heidelberg","DOI":"10.1007\/978-3-540-27813-9_29"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bozga M Iosif R Lakhnech Y (2003) Storeless semantics and alias logic. In: Proceedings of PEPM\u201903. ACM Press New York","DOI":"10.1145\/777388.777395"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"\u010ce\u0161ka M Erlebach P Vojnar T (2006) Pattern-based verification of programs with extended linear linked data structures. In: Proceedings of AVoCS\u201905. ENTCS Vol 145. Elsevier Amsterdam","DOI":"10.1016\/j.entcs.2005.10.008"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Deutsch A (1994) Interprocedural may-alias analysis for pointers: beyond k -limiting. In: Proceedings of PLDI\u201994. ACM Press New York","DOI":"10.1145\/178243.178263"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Immerman N Rabinovich A Reps T Sagiv M Yorsh G (2004) Verification via structure simulation. In: Proceedings of CAV\u201904. LNCS Vol 3114. Springer Heidelberg","DOI":"10.1007\/978-3-540-27813-9_22"},{"key":"e_1_2_1_2_7_2","unstructured":"Jonkers HBM (1981) Abstract storage structures. In: Algorithmic languages. IFIP"},{"key":"e_1_2_1_2_8_2","unstructured":"Klarlund N M\u00f8ller A (2001) MONA version 1.4 user manual. BRICS Department of Computer Science University of Aarhus"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Lee O Yang H Yi K (2005) Automatic verification of pointer programs using grammar-based shape analysis. In: Proceedings of ESOP\u201905. LNCS Vol 3444. Springer Heidelberg","DOI":"10.1007\/978-3-540-31987-0_10"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Loginov A Reps T Sagiv M (2005) Abstraction refinement via inductive learning. In: Proceedings of CAV\u201905 (to appear)","DOI":"10.1007\/11513988_50"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"M\u00f8ller A Schwartzbach MI (2001) The pointer assertion logic engine. In: Proceedings of PLDI\u201901. ACM Press New York. Also in SIGPLAN notices 36(5)","DOI":"10.1145\/381694.378851"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_1_2_13_2","unstructured":"Venet A (2005) A scalable nonuniform pointer analysis for embedded programs. In: Proceedings of SAS\u201904. LNCS Vol 3148. Springer Heidelberg"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00012-X"},{"key":"e_1_2_1_2_15_2","unstructured":"Yavuz-Kahveci T (2004) Specification and automated verification of concurrent software systems. PhD Thesis Computer Science Department of University of California"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Yavuz-Kahveci T Bultan T (2002) Automated verification of concurrent linked lists with counters. In: Proceedings of SAS\u201902. LNCS Vol 2477. Springer Heidelberg","DOI":"10.1007\/3-540-45789-5_8"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-007-0031-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-007-0031-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-007-0031-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:46:08Z","timestamp":1641483968000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-007-0031-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8]]},"references-count":16,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,8]]}},"alternative-id":["10.1007\/s00165-007-0031-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-007-0031-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,8]]}}}