Automata-Based Termination Proofs

In: Computing and Informatics, vol. 32, no. 4

R. Iosif - A. Rogalewicz

Details:

Year, pages: 2013, 739 - 775

Keywords:

Formal verification, termination analysis, Buchi automata, tree automata, programs with pointers

About article:

This paper describes our generic framework for detecting termination of programs handling infinite and complex data domains, such as pointer structures. The framework is based on a counterexample-driven abstraction refinement loop. We have instantiated the framework for programs handling tree-like data structures, which allowed us to prove automatically termination of programs such as the depth-first tree traversal, the Deutsch-Schorr-Waite tree traversal, or the linking leaves algorithm.

How to cite:

ISO 690:

Iosif, R., Rogalewicz, A. 2013. Automata-Based Termination Proofs. In Computing and Informatics, vol. 32, no.4, pp. 739-775. 1335-9150.

APA:

Iosif, R., Rogalewicz, A. (2013). Automata-Based Termination Proofs. Computing and Informatics, 32(4), 739-775. 1335-9150.