We introduce calling context graphs and various static and theorem proving based analyses that together provide a powerful method for proving termination of programs written in feature-rich, first order, functional programming languages. In contrast to previous work, our method is highly automated and handles any source of looping behavior in such languages, including recursive definitions, mutual recursion, the use of recursive data structures, etc. We have implemented our method for the ACL2 programming language and evaluated the result using the ACL2 regression suite, which consists of numerous libraries with a total of over 10,000 function definitions. Our method was able to automatically detect termination of over 98% of these functions. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Manolios, P., & Vroon, D. (2006). Termination analysis with calling context graphs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4144 LNCS, pp. 401–414). Springer Verlag. https://doi.org/10.1007/11817963_36
Mendeley helps you to discover research relevant for your work.