Búsqueda avanzada

Termination Analysis in a Multi-language Verification Platform (Trabajo en progreso)


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.

Palabras Clave:

integer automata - Termination analysis - verification platform





Este artículo tiene una licencia de uso CreativeCommons Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex