Practical Verification of Logic Program Termination

Abstract

Datalog is a simple and canonical logic programming language, variants of which are being used for data analytics and program analyses. While termination is guaranteed for programs written in pure Datalog, some variants include language features that make them Turing-complete. Krishnamurthy et al. [1996] introduce an algorithm for checking whether a program with these additional language features will terminate. We implement this algorithm and evaluate its practicality for real-world programs. We find that the algorithm does have a potential to be practical, though the current implementation does not reach this potential. We also modify the theoretical underpinnings of the algorithm’s correctness, allowing us to formally demonstrate the validity of our implementation. Finally, the results of our implementation ground a discussion of extensions of the algorithm that may lead to truly practical termination-checking for this domain.