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

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

Namespace Prefixes

PrefixIRI
n13http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n15http://localhost/temp/predkladatel/
n8http://purl.org/net/nknouf/ns/bibtex#
n9http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n4http://linked.opendata.cz/resource/domain/vavai/projekt/
n17http://linked.opendata.cz/ontology/domain/vavai/
n20https://schema.org/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n16http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F06%3APU66952%21RIV07-GA0-26230___/
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/
n14http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n18http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n7http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n19http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n5http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n12http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F06%3APU66952%21RIV07-GA0-26230___
rdf:type
skos:Concept n17:Vysledek
dcterms:description
We consider the verification of non-recursive C programs manipulating dynamic linked data structures with possibly several next pointer selectors and with finite domain non-pointer data. We aim at checking basic memory consistency properties (no null pointer assignments, etc.) and shape invariants whose violation can be expressed in an existential fragment of a first order logic over graphs. We formalise this fragment as a logic for specifying bad memory patterns whose formulae may be translated to testers written in C that can be attached to the program, thus reducing the verification problem considered to checking reachability of an error control line. We encode configurations of programs, which are essentially shape graphs, in an original way as extended tree automata and we represent program statements by tree transducers. Then, we use the abstract regular tree model checking framework for a fully automated verification. The method has been implemented and successfully applied on several case stud Článek se zabývá verifikací programů pracujících s dynamickými datovými strukturami. Každý uzel může obsahovat několik ukazatelů na následující uzly a datovou hodnotu z konečné množiny datových hodnot. Kontrolujeme zakázané manipulace s nulovými a nedefinovanými ukazateli, a dále i tvarové vlastnosti (shape properties) datové struktury. Pro specifikaci těchto vlastností používáme fragment first-order logiky nad grafy. Zakázané stavy popsané v této logice lze automaticky převést do C programu, který je přidán na konec verifikovaného programu. Tímto převedeme problem kontroly datové struktury na problem dosažitelnosti dané řádky v programu. Konfigurace programu, které jsou orientovanými grafy kódujeme jako rozšířené stromové automaty, a příkazy programu jako stromové převodníky. Poté můžeme využít metodu abstract regular tree model checking pro automatickou verifikaci těchto programů. Kompletní metoda byla implementována v prototy We consider the verification of non-recursive C programs manipulating dynamic linked data structures with possibly several next pointer selectors and with finite domain non-pointer data. We aim at checking basic memory consistency properties (no null pointer assignments, etc.) and shape invariants whose violation can be expressed in an existential fragment of a first order logic over graphs. We formalise this fragment as a logic for specifying bad memory patterns whose formulae may be translated to testers written in C that can be attached to the program, thus reducing the verification problem considered to checking reachability of an error control line. We encode configurations of programs, which are essentially shape graphs, in an original way as extended tree automata and we represent program statements by tree transducers. Then, we use the abstract regular tree model checking framework for a fully automated verification. The method has been implemented and successfully applied on several case stud
dcterms:title
Abstract Regular Tree Model Checking of Complex Dynamic Data Structures Verifikace komplexních dynamických datových struktur za použitím abstraktního regulárního stromového model checkingu Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
skos:prefLabel
Abstract Regular Tree Model Checking of Complex Dynamic Data Structures Verifikace komplexních dynamických datových struktur za použitím abstraktního regulárního stromového model checkingu Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
skos:notation
RIV/00216305:26230/06:PU66952!RIV07-GA0-26230___
n3:strany
52-69
n3:aktivita
n18:P
n3:aktivity
P(GA102/04/0780), P(GD102/05/H050), P(GP102/03/D211)
n3:dodaniDat
n12:2007
n3:domaciTvurceVysledku
n9:4978536 n9:9761985
n3:druhVysledku
n5:D
n3:duvernostUdaju
n14:S
n3:entitaPredkladatele
n16:predkladatel
n3:idSjednocenehoVysledku
463962
n3:idVysledku
RIV/00216305:26230/06:PU66952
n3:jazykVysledku
n7:eng
n3:klicovaSlova
Formal verification, symbolic verification, shape analysis, dynamic data structures, tree automata.<br>
n3:klicoveSlovo
n10:Formal%20verification n10:symbolic%20verification n10:dynamic%20data%20structures n10:shape%20analysis n10:tree%20automata.%3Cbr%3E
n3:kontrolniKodProRIV
[51C75C3AE984]
n3:mistoKonaniAkce
Seoul
n3:mistoVydani
Berlin
n3:nazevZdroje
Static Analysis
n3:obor
n19:JC
n3:pocetDomacichTvurcuVysledku
2
n3:pocetTvurcuVysledku
4
n3:projekt
n4:GD102%2F05%2FH050 n4:GP102%2F03%2FD211 n4:GA102%2F04%2F0780
n3:rokUplatneniVysledku
n12:2006
n3:tvurceVysledku
Habermehl, Peter Vojnar, Tomáš Bouajjani, Ahmed Rogalewicz, Adam
n3:typAkce
n13:WRD
n3:zahajeniAkce
2006-08-29+02:00
s:numberOfPages
18
n8:hasPublisher
Springer-Verlag
n20:isbn
3-540-37756-5
n15:organizacniJednotka
26230