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.
Publié le : 2013-11-15
Classification:
Formal verification, termination analysis, Buchi automata, tree automata, programs with pointers,
68N30, 68Q60, 68Q70, 68W30
@article{cai1970,
author = {Radu Iosif; VERIMAG, CNRS, Gi\`eres and Adam Rogalewicz; FIT, Brno University of Technology, IT4 Innovations Centre of Excellence, Brno},
title = {Automata-Based Termination Proofs},
journal = {Computing and Informatics},
volume = {31},
number = {6},
year = {2013},
language = {en},
url = {http://dml.mathdoc.fr/item/cai1970}
}
Radu Iosif; VERIMAG, CNRS, Gières; Adam Rogalewicz; FIT, Brno University of Technology, IT4 Innovations Centre of Excellence, Brno. Automata-Based Termination Proofs. Computing and Informatics, Tome 31 (2013) no. 6, . http://gdmltest.u-ga.fr/item/cai1970/