Detail publikačního výsledku

Automata-Based Termination Proofs

IOSIF, R.; ROGALEWICZ, A.

Originální název

Automata-Based Termination Proofs

Anglický název

Automata-Based Termination Proofs

Druh

Stať ve sborníku mimo WoS a Scopus

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.

Anglický 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

Klíčová slova v angličtině

Formal verification, Termination, Buchi automata, Tree automata, Programs with pointers

Autoři

IOSIF, R.; ROGALEWICZ, A.

Rok RIV

2011

Vydáno

07.07.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

Svazek

5642

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"
}