Automata-Based Termination Proofs
Keywords:Formal verification, termination analysis, Buchi automata, tree automata, programs with pointers
AbstractThis 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.
Download data is not yet available.
How to Cite
Iosif, R., & Rogalewicz, A. (2013). Automata-Based Termination Proofs. COMPUTING AND INFORMATICS, 32(4), 739–775. Retrieved from https://www.cai.sk/ojs/index.php/cai/article/view/1970