Terminator: Termination Analysis for Constraint Handling Rules

External project partner of Prof. Danny De Schreye, K.U. Leuven, Belgium, 2008-2011.

In this project, we aim to develop several new, powerful techniques for termination analysis of CHR. Our main target is to develop techniques that are able to deal with a much larger class of programs than what is currently the case. In particular, programs with propagation and simpagation rules should be in the scope of the new approach.

We will port a number of recent techniques, developed in the context of Term Rewrite Systems, such as dependency pairs, and apply them to obtain powerful termination analyzers for CHR. We will also adapt abstract interpretation for CHR to better support termination analysis. Finally, we will develop prototype systems for the most promising techniques developed in the project. We will set up a benchmark of CHR programs that form a challenge for termination analysis and we will test the implemented prototypes on this benchmark.