Automata-Based Termination Proofs

Authors

  • Radu Iosif VERIMAG, CNRS, Gières
  • Adam Rogalewicz FIT, Brno University of Technology, IT4 Innovations Centre of Excellence, Brno

Keywords:

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

Abstract

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.

Downloads

Download data is not yet available.

Downloads

Published

2013-11-15

How to Cite

Iosif, R., & Rogalewicz, A. (2013). Automata-Based Termination Proofs. Computing and Informatics, 32(4), 739–775. Retrieved from http://147.213.75.17/ojs/index.php/cai/article/view/1970

Issue

Vol. 32 No. 4 (2013): Computing and Informatics

Section

Articles