Analyzing Arithmetic Prolog Programs by Symbolic Execution
Alexander Weinert
Automated analysis of programs has been of interest for a long time now. One particular property of interest is termination behavior, that is, whether or not some program is guaranteed to terminate after a finite amount of steps.
In this work we develop an automated termination analysis for a fragment of the programming language Prolog. This fragment consists of the purely logical fragment of Prolog and the cut, as well as of arithmetic comparisons and evaluations. Even though there exist approaches that claim to analyze programs in Prolog, most of them are constrained to a small subset of the language, so-called definite programs. These approaches do not take the more complicated features of the Prolog language, such as the cut, arithmetic comparisons or arithmetic evaluations, into account.
To develop this analysis, we develop an abstract semantics that allows us to reason over sets of executions of a Prolog program written in this fragment. The objects of this semantics are abstract program graphs that describe all possible evaluations of a given query. This abstract graph-based semantics is based on existing work, which we extend to take arithmetic comparisons and evaluations into account.
We then construct an integer transition system from the abstract program graph, the termination of which implies termination of the given program. The resulting transition system can then be analyzed for termination using existing methods.
We have implemented our approach in the termination prover AProVE. Using this implementation, we have conducted experiments using a broad set of benchmarks and showed that our approach offers an improvement over existing methods, both in terms of runtime and in terms of power.
Master Thesis.