Detail publikačního výsledku

Automata-Based Termination Proofs

ROGALEWICZ, A.; IOSIF, R.

Original Title

Automata-Based Termination Proofs

English Title

Automata-Based Termination Proofs

Type

Peer-reviewed article not indexed in WoS or Scopus

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

Key words in English

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

Authors

ROGALEWICZ, A.; IOSIF, R.

RIV year

2014

Released

02.09.2013

ISBN

1335-9150

Periodical

COMPUTING AND INFORMATICS

Volume

2013

Number

4

State

Slovak Republic

Pages from

739

Pages to

775

Pages count

37

URL

http://www.cai.sk/ojs/index.php/cai/article/view/1970

Full text in the Digital Library

http://hdl.handle.net/

BibTex

@article{BUT103496,
  author="Adam {Rogalewicz} and Iosif {Radu}",
  title="Automata-Based Termination Proofs",
  journal="COMPUTING AND INFORMATICS",
  year="2013",
  volume="2013",
  number="4",
  pages="739--775",
  issn="1335-9150",
  url="http://www.cai.sk/ojs/index.php/cai/article/view/1970"
}