Termination Analysis with Calling Context Graphs
Panagiotis Manolios and Daron Vroon.
Computer-Aided Verification (CAV-2006), 2006. © Springer Verlag
Abstract
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.
PDF (184K) © Springer Verlag