CW 391

Gregory J. Duck, Tom Schrijvers, Peter J. Stuckey
An abstract interpretation framework for constraint handling rules

Abstract

Program analysis is essential for the optimized compilation of Constraint Handling Rules (CHR) as well as the inference of behavioral properties such as confluence and termination. Up to now all program analyses for CHR have been developed in an ad hoc fashion. In this work we bring the general program analysis methodology of abstract interpretation to CHR: we formulate an abstract interpretation framework over the call-based operational semantics of CHR. The abstract interpretation framework is non-obvious since it needs to handle the highly non-deterministic execution of CHRs. The use of the framework is illustrated with two instantiations: the CHR-specific late storage analysis and the more generally known groundness analysis. In addition, we discuss optimizations based on these analyses and present experimental results.