Termination Analysis in a Multi-language Verification Platform





Publicado en

Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017)

Licencia Creative Commons


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.


Acerca de Holubanský, Jakub

Palabras clave

Integer Automata, Termination Analysis, Verification Platform
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX