This HTML5 document contains 55 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n8http://localhost/temp/predkladatel/
n13http://linked.opendata.cz/resource/domain/vavai/projekt/
n9http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n12http://linked.opendata.cz/resource/domain/vavai/subjekt/
n11http://linked.opendata.cz/ontology/domain/vavai/
n20http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n4http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n19http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n16http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n17http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n15http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n18http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F11%3APU95998%21RIV12-MSM-26230___/
n14http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F11%3APU95998%21RIV12-MSM-26230___
rdf:type
skos:Concept n11:Vysledek
dcterms: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
dcterms:title
Forest Automata for Verification of Heap Manipulation Forest Automata for Verification of Heap Manipulation
skos:prefLabel
Forest Automata for Verification of Heap Manipulation Forest Automata for Verification of Heap Manipulation
skos:notation
RIV/00216305:26230/11:PU95998!RIV12-MSM-26230___
n11:predkladatel
n12:orjk%3A26230
n3:aktivita
n19:P n19:Z
n3:aktivity
P(GAP103/10/0306), P(GD102/09/H042), P(GP201/09/P531), P(MEB021023), P(OC10009), Z(MSM0021630528)
n3:cisloPeriodika
6806
n3:dodaniDat
n14:2012
n3:domaciTvurceVysledku
n9:7182430 n9:4978536 n9:9761985 n9:1258486
n3:druhVysledku
n15:J
n3:duvernostUdaju
n7:S
n3:entitaPredkladatele
n18:predkladatel
n3:idSjednocenehoVysledku
200113
n3:idVysledku
RIV/00216305:26230/11:PU95998
n3:jazykVysledku
n16:eng
n3:klicovaSlova
shape analysis, dynamic linked data structures, tree automata, trees, linked lists, formal verification, abstract regular model checking
n3:klicoveSlovo
n4:formal%20verification n4:dynamic%20linked%20data%20structures n4:trees n4:shape%20analysis n4:tree%20automata n4:abstract%20regular%20model%20checking n4:linked%20lists
n3:kodStatuVydavatele
DE - Spolková republika Německo
n3:kontrolniKodProRIV
[CA0FA375C19C]
n3:nazevZdroje
Lecture Notes in Computer Science (IF 0,513)
n3:obor
n17:IN
n3:pocetDomacichTvurcuVysledku
4
n3:pocetTvurcuVysledku
5
n3:projekt
n13:GAP103%2F10%2F0306 n13:GP201%2F09%2FP531 n13:GD102%2F09%2FH042 n13:OC10009 n13:MEB021023
n3:rokUplatneniVysledku
n14:2011
n3:svazekPeriodika
2011
n3:tvurceVysledku
Rogalewicz, Adam Habermehl, Peter Vojnar, Tomáš Holík, Lukáš Šimáček, Jiří
n3:zamer
n20:MSM0021630528
s:issn
0302-9743
s:numberOfPages
16
n8:organizacniJednotka
26230