Automata-Based Termination Proofs

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F13%3APU106356" target="_blank" >RIV/00216305:26230/13:PU106356 - isvavai.cz</a>

Result on the web

<a href="http://www.cai.sk/ojs/index.php/cai/article/view/1970" target="_blank" >http://www.cai.sk/ojs/index.php/cai/article/view/1970</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Automata-Based Termination Proofs

Original language 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 linking leaves algorithm.

Czech name

—

Czech description

—

Type

J_ost - Miscellaneous article in a specialist periodical

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2013

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Computing and Informatics

ISSN

1335-9150

e-ISSN

—

Volume of the periodical

2013

Issue of the periodical within the volume

4

Country of publishing house

SK - SLOVAKIA

Number of pages

37

Pages from-to

739-775

UT code for WoS article

—

EID of the result in the Scopus database

—