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

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

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n13http://localhost/temp/predkladatel/
n19http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n17http://linked.opendata.cz/resource/domain/vavai/projekt/
n18http://linked.opendata.cz/resource/domain/vavai/subjekt/
n15http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216305%3A26230%2F13%3APU106356%21RIV14-GA0-26230___/
n7http://linked.opendata.cz/ontology/domain/vavai/
n6http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n4http://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/
n5http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n16http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n20http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n10http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n14http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216305%3A26230%2F13%3APU106356%21RIV14-GA0-26230___
rdf:type
n7:Vysledek skos:Concept
dcterms:description
This paper proposes a framework for detecting termination of programs handling infinite and complex data domains, such as pointer structures. In this framework, the user has to specify a finite number of well-founded relations on the data domain manipulated by these programs. Our tool then builds an initial abstraction of the program, which is checked for existence of potential infinite runs, by testing emptiness of its intersection with a predefined Buchi automaton. If the intersection is non-empty, a lasso-shaped counterexample is found. This counterexample is checked for spuriousness by a domain-specific procedure, and in case it is found to be spurious, the abstraction is refined, again by intersection with the complement of the Buchi automaton representing the lasso. We have instantiated the framework for programs handling tree-like data structures, which allowed us to prove termination of programs such as the depth-first tree traversal, the Deutsch-Schorr-Waite tree traversal, or the This paper proposes a framework for detecting termination of programs handling infinite and complex data domains, such as pointer structures. In this framework, the user has to specify a finite number of well-founded relations on the data domain manipulated by these programs. Our tool then builds an initial abstraction of the program, which is checked for existence of potential infinite runs, by testing emptiness of its intersection with a predefined Buchi automaton. If the intersection is non-empty, a lasso-shaped counterexample is found. This counterexample is checked for spuriousness by a domain-specific procedure, and in case it is found to be spurious, the abstraction is refined, again by intersection with the complement of the Buchi automaton representing the lasso. We have instantiated the framework for programs handling tree-like data structures, which allowed us to prove termination of programs such as the depth-first tree traversal, the Deutsch-Schorr-Waite tree traversal, or the
dcterms:title
Automata-Based Termination Proofs Automata-Based Termination Proofs
skos:prefLabel
Automata-Based Termination Proofs Automata-Based Termination Proofs
skos:notation
RIV/00216305:26230/13:PU106356!RIV14-GA0-26230___
n7:predkladatel
n18:orjk%3A26230
n4:aktivita
n12:S n12:P n12:Z
n4:aktivity
P(ED1.1.00/02.0070), P(GAP103/10/0306), S, Z(MSM0021630528)
n4:cisloPeriodika
4
n4:dodaniDat
n14:2014
n4:domaciTvurceVysledku
n19:4978536
n4:druhVysledku
n10:J
n4:duvernostUdaju
n5:S
n4:entitaPredkladatele
n15:predkladatel
n4:idSjednocenehoVysledku
62557
n4:idVysledku
RIV/00216305:26230/13:PU106356
n4:jazykVysledku
n16:eng
n4:klicovaSlova
Formal verification, Termination, Buchi automata, Tree automata, Programs with pointers
n4:klicoveSlovo
n11:Formal%20verification n11:Tree%20automata n11:Termination n11:Programs%20with%20pointers n11:Buchi%20automata
n4:kodStatuVydavatele
SK - Slovenská republika
n4:kontrolniKodProRIV
[B45F03168A7B]
n4:nazevZdroje
Computing and Informatics
n4:obor
n20:IN
n4:pocetDomacichTvurcuVysledku
1
n4:pocetTvurcuVysledku
2
n4:projekt
n17:GAP103%2F10%2F0306 n17:ED1.1.00%2F02.0070
n4:rokUplatneniVysledku
n14:2013
n4:svazekPeriodika
2013
n4:tvurceVysledku
Radu, Iosif Rogalewicz, Adam
n4:zamer
n6:MSM0021630528
s:issn
1335-9150
s:numberOfPages
37
n13:organizacniJednotka
26230