Applying static analysis techniques for inferring termination conditions of logic programs

Fred Mesnard Ulrich Neumerkel

To appear at Static Analysis Symposium (SAS01), Paris, France, 16-18 July 2001


Abstract

We present the implementation of cTI, a system for universal left-termination inference of logic programs, which heavily relies on static analysis techniques. Termination inference generalizes termination analysis/checking. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided to the system, requiring user annotations. With termination inference such annotations are no longer necessary. Instead, all provably terminating classes to all related predicates are inferred at once. The architecture of cTI is described and some optimizations are discussed. Running times for classical examples from the termination literature in LP and for some middle-sized logic programs are given.


Server START Conference Manager
Update Time 31 Mar 2001 at 16:55:39
Maintainer sas01@ens.fr.
Start Conference Manager
Conference Systems