Applying Static Analysis Techniques for Inferring Termination Conditions of Logic Programs

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 not 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.

• Type: Conference
• Year: 2001
• Where: SAS
• Authors: Frédéric Mesnard, Ulrich Neumerkel
• Keywords: Formal Methods, Inference Generalizes Termination, Logic Programs, SAS 2001, Termination Inference