Publication detail
Automata-Based Termination Proofs
IOSIF, R. ROGALEWICZ, A.
Original Title
Automata-Based Termination Proofs
English Title
Automata-Based Termination Proofs
Type
conference paper
Language
en
Original Abstract
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.
English abstract
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.
Keywords
Formal verification, Termination, Buchi automata, Tree automata, Programs with pointers
RIV year
2009
Released
07.07.2009
Publisher
Springer Verlag
Location
Berlin
ISBN
978-3-642-02978-3
Book
Implementation and Application of Automata
Edition
Lecture Notes in Computer Science
Edition number
NEUVEDEN
Pages from
165
Pages to
177
Pages count
13
URL
Documents
BibTex
@inproceedings{BUT30222,
author="Iosif {Radu} and Adam {Rogalewicz}",
title="Automata-Based Termination Proofs",
annote="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.",
address="Springer Verlag",
booktitle="Implementation and Application of Automata",
chapter="30222",
edition="Lecture Notes in Computer Science",
howpublished="print",
institution="Springer Verlag",
year="2009",
month="july",
pages="165--177",
publisher="Springer Verlag",
type="conference paper"
}