About: Automata-Based Termination Proofs

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

About: Automata-Based Termination Proofs 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 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 (en)
Title	Automata-Based Termination Proofs Automata-Based Termination Proofs (en)
skos:prefLabel	Automata-Based Termination Proofs Automata-Based Termination Proofs (en)
skos:notation	RIV/00216305:26230/13:PU106356!RIV14-GA0-26230___
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(ED1.1.00/02.0070), P(GAP103/10/0306), S, Z(MSM0021630528)
http://linked.open...iv/cisloPeriodika	4
http://linked.open...vai/riv/dodaniDat	2014
http://linked.open...aciTvurceVysledku	Rogalewicz, Adam
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
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	62557
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/13:PU106356
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	Formal verification, Termination, Buchi automata, Tree automata, Programs with pointers (en)
http://linked.open.../riv/klicoveSlovo	Buchi automata Programs with pointers Tree automata Termination Formal verification
http://linked.open...odStatuVydavatele	SK - Slovenská republika
http://linked.open...ontrolniKodProRIV	[B45F03168A7B]
http://linked.open...i/riv/nazevZdroje	Computing and Informatics
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	2 (xsd:int)
http://linked.open...vavai/riv/projekt	IT4Innovations Centre of Excellence Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness
http://linked.open...UplatneniVysledku	2013
http://linked.open...v/svazekPeriodika	2013
http://linked.open...iv/tvurceVysledku	Rogalewicz, Adam Radu, Iosif
http://linked.open...n/vavai/riv/zamer	Výzkum informačních technologií z hlediska bezpečnosti
issn	1335-9150
number of pages	37 (xsd:int)
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