Automatic Termination Analysis

Abstract Proving termination of programs is important in any approach to program development. In logic programming, where the logic and the control component of a program can very easily be dealt with in two separate phases of the development, the termination issue is solely addressed in the second phase. Both formal, theoretical frameworks for reasoning about termination, and automatic techniques for termination analysis have recently obtained considerable attention in the logic programming community. Unfortunately, in current work, these two types of approaches to termination have been rather orthogonal. It would be desirable if automatic techniques could rely directly on general frameworks for their correctness proofs. We recently presented a new, practical framework for termination analysis of definite logic programs with respect to call patterns. In the current paper, we describe an automated technique, which is directly based on the framework. The main advantages are: the generality of the approach (analysis can be performed for any given set of top-level goals), the clear theoretical underpinning provided by the framework and full automation. .

Authors

• Kristof Verschaetse
• Stefaan Decorte
• Danny De Schreye

Keywords

No keywords are indexed for this paper.