CW 2003_02

A. Serebrenik
Termination analysis of logic programs

Advisor: D. De Schreye

Abstract

Termination is well-known to be one of the most intriguing aspects of program verification. In context of logic programming, where logic and control aspects of a program are separated, termination is considered as an important issue in control generation. Since logic programs are Turing-complete, it follows by the undecidability of the halting problem that there exists no algorithm which, given an arbitrary logic program, decides whether the program terminates. However, one can propose both conditions that are equivalent to termination and their approximations that imply termination and can be verified automatically. These kinds of conditions are discussed in the thesis.

Our achievements are twofold. First, I developed a framework for integration of general orderings within the well-known context of acceptability with respect to a set. The methodology developed allowed me to bridge a gap between two major approaches to termination analysis: the transformational approach and the direct approach. This framework plays a key role in the study of the termination behaviour of meta-interpreters. Secondly, I turned my attention to programs with numerical computations. While such programs are very common in real-world programming, until recent they mostly remained a terra incognita for the research community. First integer computations were considered, the crucial obstacle there being the lack of well-foundedness of integers. Then this work was extended to computations which depend on floating point numbers. Unlike theoretical objects, such as real numbers, floating point numbers are the numbers represented by computers. Thus, imprecision and rounding errors are intrinsic to computations involving floating point numbers. This issue constituted the main challenge in this case. To the best of my knowledge, the results presented constitute the first work on termination in the context of floating point computations. It should also be stressed that although the results are stated in logic programming language, they are not bound to logic programming,because the matters considered do not depend on the logical aspects of the language.