Title: A new approach to non-termination analysis of Logic Programs
Authors: Voets, Dean
De Schreye, Danny
Issue Date: Mar-2009
Publisher: Department of Computer Science, K.U.Leuven
Series Title: CW Reports vol:CW537
Abstract: In this paper, we present a new approach to non-termination analysis of logic programs based on moded SLDNF-resolution. Moded SLDNF-resolution is a symbolic execution for moded goals developed for termination prediction. To prove non-termination, we use a complete loop checker to create a finite symbolic derivation tree of a logic program and moded query. Then, we check if this derivation tree contains an infinite loop, using a new non-termination condition. We implemented this approach and tested it on the benchmark from the Termination Competition of 2007. The results are very satisfactory: our tool is able to prove non-termination and construct non-terminating queries for all non-terminating benchmark programs, and thus, significantly improves on the results of the only other non-termination analyzer, NTI.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
cw537.pdfMain article Published 323KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.