Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
IOSIF, R. ROGALEWICZ, A.
Originální název
Automata-Based Termination Proofs
Typ
článek ve sborníku mimo WoS a Scopus
Jazyk
angličtina
Originální abstrakt
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.
Klíčová slova
Formal verification, Termination, Buchi automata, Tree automata, Programs with pointers
Autoři
IOSIF, R.; ROGALEWICZ, A.
Rok RIV
2009
Vydáno
7. 7. 2009
Nakladatel
Springer Verlag
Místo
Berlin
ISBN
978-3-642-02978-3
Kniha
Implementation and Application of Automata
Edice
Lecture Notes in Computer Science
Strany od
165
Strany do
177
Strany počet
13
URL
http://www.springerlink.com/content/j026j27j77284lu3/fulltext.pdf
BibTex
@inproceedings{BUT30222, author="Iosif {Radu} and Adam {Rogalewicz}", title="Automata-Based Termination Proofs", booktitle="Implementation and Application of Automata", year="2009", series="Lecture Notes in Computer Science", volume="5642", pages="165--177", publisher="Springer Verlag", address="Berlin", isbn="978-3-642-02978-3", url="http://www.springerlink.com/content/j026j27j77284lu3/fulltext.pdf" }