Automata-Based Termination Proofs
Result 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 domainmanipulated 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 complementof 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 Deu
Keywords
Formal verificationTerminationBuchi automataTree automataPrograms with pointers
The result's identifiers
Result code in IS VaVaI
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
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 domainmanipulated 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 complementof 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 DeuCzech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
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)
Others
Publication year
2009
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Implementation and Application of Automata
ISBN
978-3-642-02978-3
ISSN
—
e-ISSN
—
Number of pages
13
Pages from-to
—
Publisher name
Springer Verlag
Place of publication
Berlin
Event location
Sydney
Event date
Apr 14, 2009
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—
Basic information
Result type
D - Article in proceedings
CEP
JC - Computer hardware and software
Year of implementation
2009