Resumen:
One aim of the verification platform CAVI-ART is to provide as much assistance as possible to programmers in order to alleviate their verification effort. One of these aids is automatically proving termination of programs, whenever this is possible. Since CAVI-ART is a multi-language platform, the analysis is performed at the level of the platform Intermediate Representation language (IR), to which all source languages are first translated.
We have selected one of the the most successful termination tools, called RANK, and transform our IR-programs to an appropriate input for RANK. There is a fundamental mismatch between the functional, stateless, recursive flavour of our IR, and the automaton-based input of RANK, which is a tool developed for imperative, mutable-state programs. In this paper we show how we have circumvented this problem, and present an algorithm transforming the IR to an automaton. We give some examples of recursive programs that we have successfully proved terminating.