SwePub
Sök i LIBRIS databas

  Extended search

L773:0925 9856 OR L773:1572 8102
 

Search: L773:0925 9856 OR L773:1572 8102 > (2010-2014) > Forest automata for...

Forest automata for verification of heap manipulation

Habermehl, Peter (author)
Holík, Lukáš (author)
Uppsala universitet,Datorteknik
Rogalewicz, Adam (author)
show more...
Šimáček, Jiří (author)
Vojnar, Tomas (author)
show less...
 (creator_code:org_t)
2012-04-11
2012
English.
In: Formal methods in system design. - : Springer Science and Business Media LLC. - 0925-9856 .- 1572-8102. ; 41:1, s. 83-106
  • Journal article (peer-reviewed)
Abstract Subject headings
Close  
  • 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.

Subject headings

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

Keyword

Pointers
Shape analysis
Regular model checking
Tree automata

Publication and Content Type

ref (subject category)
art (subject category)

Find in a library

To the university's database

Search outside SwePub

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.

 
pil uppåt Close

Copy and save the link in order to return to this view