About: Automata-based Verification of Programs with Tree Updates

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

About: Automata-based Verification of Programs with Tree Updates 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	This paper describes an effective verification procedure for imperative programs that handle (balanced) tree-like data structures. Since the verification problem considered is undecidable, we appeal to a classical semi-algorithmic approach in which the user has to provide manually the loop invariants in order to check the validity of Hoare triples of the form {P}C{Q}, where P, Q are the sets of states corresponding to the pre- and post-conditions, and C is the program to be verified. We specify the sets of states (representing tree-like memory configurations) using  a special class of tree automata named Tree Automata with Size Constraints (TASC). The main advantage of using TASC in program specifications is that they recognize non-regular sets of tree languages such as the <i>AVL trees</i>, the  <i>red-black trees</i>, and in general, specifications involving arithmetic reasoning about the lengths (depths) of various (possibly all) paths in the tree. The class of TASC is closed under the op This paper describes an effective verification procedure for imperative programs that handle (balanced) tree-like data structures. Since the verification problem considered is undecidable, we appeal to a classical semi-algorithmic approach in which the user has to provide manually the loop invariants in order to check the validity of Hoare triples of the form {P}C{Q}, where P, Q are the sets of states corresponding to the pre- and post-conditions, and C is the program to be verified. We specify the sets of states (representing tree-like memory configurations) using  a special class of tree automata named Tree Automata with Size Constraints (TASC). The main advantage of using TASC in program specifications is that they recognize non-regular sets of tree languages such as the <i>AVL trees</i>, the  <i>red-black trees</i>, and in general, specifications involving arithmetic reasoning about the lengths (depths) of various (possibly all) paths in the tree. The class of TASC is closed under the op (en)
Title	Automata-based Verification of Programs with Tree Updates Automata-based Verification of Programs with Tree Updates (en)
skos:prefLabel	Automata-based Verification of Programs with Tree Updates Automata-based Verification of Programs with Tree Updates (en)
skos:notation	RIV/00216305:26230/06:PU66868!RIV10-GA0-26230___
http://linked.open...avai/riv/aktivita	P
http://linked.open...avai/riv/aktivity	P(GA102/04/0780), P(GP102/03/D211)
http://linked.open...vai/riv/dodaniDat	2010
http://linked.open...aciTvurceVysledku	Vojnar, Tomáš
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
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	466375
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/06:PU66868
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Formal verification, symbolic verification, programs handling balanced trees, theory of automata.<br> (en)
http://linked.open.../riv/klicoveSlovo	Formal verification programs handling balanced trees symbolic verification theory of automata.<br>
http://linked.open...ontrolniKodProRIV	[ABB3B51D3090]
http://linked.open...v/mistoKonaniAkce	Vienna
http://linked.open...i/riv/mistoVydani	Berlin
http://linked.open...i/riv/nazevZdroje	Tools and Algorithms for the Construction and Analysis of Systems
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	Advanced Methods of Automatic Verification of Parametric and Infinite-State Systems Automated methods and tools supporting development of reliable concurrent and distributed systems
http://linked.open...UplatneniVysledku	2006
http://linked.open...iv/tvurceVysledku	Vojnar, Tomáš Habermehl, Peter Radu, Iosif
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2006-03-25 (xsd:date)
number of pages	15 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	978-3-540-33056-1
http://localhost/t...ganizacniJednotka	26230

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, 77 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software