About: Forest Automata for Verification of Heap Manipulation

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Forest Automata for Verification of Heap Manipulation Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
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	Fakulta informačních technologií
http://linked.open...avai/riv/aktivita	P Z
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	6806
http://linked.open...vai/riv/dodaniDat	2012
http://linked.open...aciTvurceVysledku	Šimáček, Jiří Holík, Lukáš Vojnar, Tomáš Rogalewicz, Adam
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Vysoké učení technické v Brně / Fakulta informačních technologií
http://linked.open...dnocenehoVysledku	200113
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/11:PU95998
http://linked.open...riv/jazykVysledku	eng - angličtina
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	abstract regular model checking dynamic linked data structures linked lists shape analysis trees formal verification tree automata
http://linked.open...odStatuVydavatele	DE - Spolková republika Německo
http://linked.open...ontrolniKodProRIV	[CA0FA375C19C]
http://linked.open...i/riv/nazevZdroje	Lecture Notes in Computer Science (IF 0,513)
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	4 (xsd:int)
http://linked.open...cetTvurcuVysledku	5 (xsd:int)
http://linked.open...vavai/riv/projekt	Developement of methods for automatic verification of programs with dynamic data structures Automata and Logic for Symbolic Verification of Software Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit
http://linked.open...UplatneniVysledku	2011
http://linked.open...v/svazekPeriodika	2011
http://linked.open...iv/tvurceVysledku	Holík, Lukáš Vojnar, Tomáš Šimáček, Jiří Habermehl, Peter Rogalewicz, Adam
http://linked.open...n/vavai/riv/zamer	Výzkum informačních technologií z hlediska bezpečnosti
issn	0302-9743
number of pages	16 (xsd:int)
http://localhost/t...ganizacniJednotka	26230
is http://linked.open...avai/riv/vysledek of	Forest Automata for Verification of Heap Manipulation Forest Automata for Verification of Heap Manipulation

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 41 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software