uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Forest automata for verification of heap manipulation
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Show others and affiliations
2012 (English)In: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 41, no 1, 83-106 p.Article in journal (Refereed) Published
Abstract [en]

We consider verification of programs manipulating dynamic linked data structures such as various forms of singly and doubly-linked lists or trees. We consider important properties for this kind of systems like no null-pointer dereferences, absence of garbage, shape properties, etc. We develop a verification method based on a novel use of tree automata to represent heap configurations. A heap is split into several "separated" parts such that each of them can be represented by a tree automaton. The automata can refer to each other allowing the different parts of the heaps to mutually refer to their boundaries. Moreover, we allow for a hierarchical representation of heaps by allowing alphabets of the tree automata to contain other, nested tree automata. Program instructions can be easily encoded as operations on our representation structure. This allows verification of programs based on symbolic state-space exploration together with refinable abstraction within the so-called abstract regular tree model checking. A motivation for the approach is to combine advantages of automata-based approaches (higher generality and flexibility of the abstraction) with some advantages of separation-logic-based approaches (efficiency). We have implemented our approach and tested it successfully on multiple non-trivial case studies.

Place, publisher, year, edition, pages
2012. Vol. 41, no 1, 83-106 p.
Keyword [en]
Pointers, Shape analysis, Regular model checking, Tree automata
National Category
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-178071DOI: 10.1007/s10703-012-0150-8ISI: 000305785600006OAI: oai:DiVA.org:uu-178071DiVA: diva2:542155
Available from: 2012-07-30 Created: 2012-07-27 Last updated: 2017-12-07Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Holík, Lukáš

Search in DiVA

By author/editor
Holík, Lukáš
By organisation
Computer Systems
In the same journal
Formal methods in system design
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 421 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf