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.
Keywords
MSC
68N30, 68Q60, 68Q70, 68W30
Cite this article
@article{cai-110141,
author = {Radu Iosif and Adam Rogalewicz},
title = {Automata-Based Termination Proofs},
journal = {Computing and Informatics},
volume = {32},
number = {4},
pages = {739--775},
year = {2013},
issn = {1335-9150},
url = {https://cai.type.sk/content/2013/4/automata-based-termination-proofs/}
}
TY - JOUR AU - Radu Iosif AU - Adam Rogalewicz TI - Automata-Based Termination Proofs JO - Computing and Informatics VL - 32 IS - 4 SP - 739 EP - 775 PY - 2013 SN - 1335-9150 UR - https://cai.type.sk/content/2013/4/automata-based-termination-proofs/ KW - Formal verification KW - termination analysis KW - Buchi automata KW - tree automata KW - programs with pointers ER -
Iosif, R., & Rogalewicz, A. (2013). Automata-Based Termination Proofs. Computing and Informatics, 32(4), 739–775. https://cai.type.sk/content/2013/4/automata-based-termination-proofs/