Detail publikace

Automata-Based Termination Proofs

Originální název

Automata-Based Termination Proofs

Anglický název

Automata-Based Termination Proofs

Jazyk

en

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.

BibTex


@article{BUT103496,
  author="Adam {Rogalewicz} and Iosif {Radu}",
  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="NEUVEDEN",
  chapter="103496",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="4",
  volume="2013",
  year="2013",
  month="september",
  pages="739--775",
  publisher="NEUVEDEN",
  type="journal article - other"
}