Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-18T12:32:02.982Z Has data issue: false hasContentIssue false
  • English
  • Français

Inferring termination conditions for logic programs using backwards analysis

Published online by Cambridge University Press:  10 January 2005

SAMIR GENAIM  and
MICHAEL CODISH
SAMIR GENAIM
Affiliation:
Dipartimento di Informatica, Università degli Studi di Verona, Verona, Italy (e-mail: [email protected])
MICHAEL CODISH
Affiliation:
Department of Computer Science, Ben-Gurion University, Israel (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper focuses on the inference of modes for which a logic program is guaranteed to terminate. This generalises traditional termination analysis where an analyser tries to verify termination for a specified mode. Our contribution is a methodology in which components of traditional termination analysis are combined with backwards analysis to obtain an analyser for termination inference. We identify a condition on the components of the analyser which guarantees that termination inference will infer all modes which can be checked to terminate. The application of this methodology to enhance a traditional termination analyser to perform also termination inference is demonstrated.

Keywords

program analysisabstract interpretationtermination analysisbackwards analysis
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 5 , Issue 1-2 , January 2005 , pp. 75 - 91
Copyright
© 2005 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)