Automatic termination analysis of programs containing arithmetic predicates

N. Dershowitz, N. Lindenstrauss, Y. Sagiv, A. Serebrenik

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)

    Abstract

    For logic programs with arithmetic predicates, showing termination is not easy, since the usual order for the integers is not well-founded. A new method, easily incorporated in the TermiLog system for automatic termination analysis, is presented for showing termination in this case. The method consists of the following steps: First, a finite abstract domain for representing the range of integers is deduced automatically. Based on this abstraction, abstract interpretation is applied to the program. The result is a finite number of atoms abstracting answers to queries which are used to extend the technique of query-mapping pairs. For each query-mapping pair that is potentially non-terminating, a bounded (integer-valued) termination function is guessed. If traversing the pair decreases the value of the termination function, then termination is established. Simple functions often suffice for each query-mapping pair, and that gives our approach an edge over the classical approach of using a single termination function for all loops, which must inevitably be more complicated and harder to guess automatically. It is worth noting that the termination of McCarthy's 91 function can be shown automatically using our method. In summary, the proposed approach is based on combining a finite abstraction of the integers with the technique of the query-mapping pairs, and is essentially capable of dividing a termination proof into several cases, such that a simple termination function suffices for each case. Consequently, the whole process of proving termination can be done automatically in the framework of TermiLog and similar systems.
    Original languageEnglish
    Title of host publicationWorkshop on Verification of Logic Programs (in connection with ICLP'99, International Conference on Logic Programming, Las Cruces NM, USA, December 1, 1999)
    EditorsS. Etalle, J.G. Smaus
    Pages39-58
    DOIs
    Publication statusPublished - 1999

    Publication series

    NameElectronic Notes in Theoretical Computer Science
    Volume30(1)
    ISSN (Print)1571-0061

    Fingerprint

    Dive into the research topics of 'Automatic termination analysis of programs containing arithmetic predicates'. Together they form a unique fingerprint.

    Cite this