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

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

Namespace Prefixes

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

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F07%3APU70921%21RIV08-MSM-26230___
rdf:type
skos:Concept n12:Vysledek
dcterms:description
We focus in details on the use of abstract regular tree model checking (ARTMC) within a successful method for verification of programs with dynamic data structures. The method is based on a use of a set of transducers to describe the behaviour of the verified system. But the ARTMC method was originally developed for systems of one transducer only and its generalization to several ones was supposed to be straightforward. Although this straightforward generalization (used in a prototype&nbsp; implementation) works well in a number of examples, the counterexample analysis is in general unreliable and can cause infinite looping of the tool as we demonstrate on a simple example containing an erroneous pointer manipulation. Therefore we propose a new&nbsp; algorithm used for a counterexample analysis and we prove its correctness. We focus in details on the use of abstract regular tree model checking (ARTMC) within a successful method for verification of programs with dynamic data structures. The method is based on a use of a set of transducers to describe the behaviour of the verified system. But the ARTMC method was originally developed for systems of one transducer only and its generalization to several ones was supposed to be straightforward. Although this straightforward generalization (used in a prototype&nbsp; implementation) works well in a number of examples, the counterexample analysis is in general unreliable and can cause infinite looping of the tool as we demonstrate on a simple example containing an erroneous pointer manipulation. Therefore we propose a new&nbsp; algorithm used for a counterexample analysis and we prove its correctness. Článek studuje použití abstraktního regulárního model checkingu, uvnitř úspěšné metody pro verifikace programů se složitými datovými strukturami, a to zejména analýza protipříkladů.<br>
dcterms:title
Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures Analýza protipříkladů v abstraktním regulárním model checkingu pro složité dynamické datové struktury Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
skos:prefLabel
Analýza protipříkladů v abstraktním regulárním model checkingu pro složité dynamické datové struktury Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
skos:notation
RIV/00216305:26230/07:PU70921!RIV08-MSM-26230___
n3:strany
59-66
n3:aktivita
n15:P n15:Z
n3:aktivity
P(GD102/05/H050), Z(MSM0021630528)
n3:dodaniDat
n8:2008
n3:domaciTvurceVysledku
n20:4978536 n20:1258486
n3:druhVysledku
n13:D
n3:duvernostUdaju
n18:S
n3:entitaPredkladatele
n10:predkladatel
n3:idSjednocenehoVysledku
415189
n3:idVysledku
RIV/00216305:26230/07:PU70921
n3:jazykVysledku
n9:eng
n3:klicovaSlova
Formal verification, Regular tree model checking, shape analysis, <br>
n3:klicoveSlovo
n11:%3Cbr%3E n11:Formal%20verification n11:Regular%20tree%20model%20checking n11:shape%20analysis
n3:kontrolniKodProRIV
[5016F15BF99A]
n3:mistoKonaniAkce
Znojmo
n3:mistoVydani
Znojmo
n3:nazevZdroje
Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007)
n3:obor
n4:JC
n3:pocetDomacichTvurcuVysledku
2
n3:pocetTvurcuVysledku
2
n3:projekt
n14:GD102%2F05%2FH050
n3:rokUplatneniVysledku
n8:2007
n3:tvurceVysledku
Holík, Lukáš Rogalewicz, Adam
n3:typAkce
n19:WRD
n3:zahajeniAkce
2007-10-26+02:00
n3:zamer
n17:MSM0021630528
s:numberOfPages
8
n16:hasPublisher
Neuveden
n22:isbn
978-80-7355-077-6
n7:organizacniJednotka
26230