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

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

Namespace Prefixes

PrefixIRI
n4http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n21http://localhost/temp/predkladatel/
n14http://purl.org/net/nknouf/ns/bibtex#
n20http://linked.opendata.cz/resource/domain/vavai/projekt/
n16http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n15http://linked.opendata.cz/ontology/domain/vavai/
n18https://schema.org/
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#
n10http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n9http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n17http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n13http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n19http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n6http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F06%3APU66868%21RIV10-GA0-26230___/
n7http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F06%3APU66868%21RIV10-GA0-26230___
rdf:type
skos:Concept n15:Vysledek
dcterms: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&nbsp; 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&nbsp; <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&nbsp; 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&nbsp; <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
dcterms:title
Automata-based Verification of Programs with Tree Updates Automata-based Verification of Programs with Tree Updates
skos:prefLabel
Automata-based Verification of Programs with Tree Updates Automata-based Verification of Programs with Tree Updates
skos:notation
RIV/00216305:26230/06:PU66868!RIV10-GA0-26230___
n3:aktivita
n13:P
n3:aktivity
P(GA102/04/0780), P(GP102/03/D211)
n3:dodaniDat
n7:2010
n3:domaciTvurceVysledku
n16:9761985
n3:druhVysledku
n19:D
n3:duvernostUdaju
n9:S
n3:entitaPredkladatele
n6:predkladatel
n3:idSjednocenehoVysledku
466375
n3:idVysledku
RIV/00216305:26230/06:PU66868
n3:jazykVysledku
n17:eng
n3:klicovaSlova
Formal verification, symbolic verification, programs handling balanced trees, theory of automata.<br>
n3:klicoveSlovo
n10:theory%20of%20automata.%3Cbr%3E n10:programs%20handling%20balanced%20trees n10:symbolic%20verification n10:Formal%20verification
n3:kontrolniKodProRIV
[ABB3B51D3090]
n3:mistoKonaniAkce
Vienna
n3:mistoVydani
Berlin
n3:nazevZdroje
Tools and Algorithms for the Construction and Analysis of Systems
n3:obor
n12:JC
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
3
n3:projekt
n20:GA102%2F04%2F0780 n20:GP102%2F03%2FD211
n3:rokUplatneniVysledku
n7:2006
n3:tvurceVysledku
Vojnar, Tomáš Habermehl, Peter Radu, Iosif
n3:typAkce
n4:WRD
n3:zahajeniAkce
2006-03-25+01:00
s:numberOfPages
15
n14:hasPublisher
Springer-Verlag
n18:isbn
978-3-540-33056-1
n21:organizacniJednotka
26230