Attributes | Values |
---|
rdf:type
| |
Description
| - 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 %22separated%22 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 a symbolic state-space exploration together with refinable abstraction within the so-called abstract regula
- 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 %22separated%22 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 a symbolic state-space exploration together with refinable abstraction within the so-called abstract regula (en)
|
Title
| - Forest Automata for Verification of Heap Manipulation
- Forest Automata for Verification of Heap Manipulation (en)
|
skos:prefLabel
| - Forest Automata for Verification of Heap Manipulation
- Forest Automata for Verification of Heap Manipulation (en)
|
skos:notation
| - RIV/00216305:26230/11:PU95998!RIV12-MSM-26230___
|
http://linked.open...avai/predkladatel
| |
http://linked.open...avai/riv/aktivita
| |
http://linked.open...avai/riv/aktivity
| - P(GAP103/10/0306), P(GD102/09/H042), P(GP201/09/P531), P(MEB021023), P(OC10009), Z(MSM0021630528)
|
http://linked.open...iv/cisloPeriodika
| |
http://linked.open...vai/riv/dodaniDat
| |
http://linked.open...aciTvurceVysledku
| |
http://linked.open.../riv/druhVysledku
| |
http://linked.open...iv/duvernostUdaju
| |
http://linked.open...titaPredkladatele
| |
http://linked.open...dnocenehoVysledku
| |
http://linked.open...ai/riv/idVysledku
| - RIV/00216305:26230/11:PU95998
|
http://linked.open...riv/jazykVysledku
| |
http://linked.open.../riv/klicovaSlova
| - shape analysis, dynamic linked data structures, tree automata, trees, linked lists, formal verification, abstract regular model checking (en)
|
http://linked.open.../riv/klicoveSlovo
| |
http://linked.open...odStatuVydavatele
| - DE - Spolková republika Německo
|
http://linked.open...ontrolniKodProRIV
| |
http://linked.open...i/riv/nazevZdroje
| - Lecture Notes in Computer Science (IF 0,513)
|
http://linked.open...in/vavai/riv/obor
| |
http://linked.open...ichTvurcuVysledku
| |
http://linked.open...cetTvurcuVysledku
| |
http://linked.open...vavai/riv/projekt
| |
http://linked.open...UplatneniVysledku
| |
http://linked.open...v/svazekPeriodika
| |
http://linked.open...iv/tvurceVysledku
| - Holík, Lukáš
- Vojnar, Tomáš
- Šimáček, Jiří
- Habermehl, Peter
- Rogalewicz, Adam
|
http://linked.open...n/vavai/riv/zamer
| |
issn
| |
number of pages
| |
http://localhost/t...ganizacniJednotka
| |
is http://linked.open...avai/riv/vysledek
of | |