Domain Independent Ask Approximation in CCP

The main difficulty in the formalization of a static analysis framework for CC programs is probably related to the correct approximation of the entailment relation between constraints. This approximation is needed for the abstract evaluation of the ask guards and directly influences the overall precision of the analysis. In this paper we provide a solution to this problem by stating reasonable correctness conditions relating the abstract and the concrete domains of computation. The solution is domain independent in the sense that it can be applied to the class of downward closed observables. Properties falling in this class have already been studied in the context of the analysis of sequential (conlogic programs. As an example, we consider an abstract domain designed for the analysis of freeness in CLP programs and we show how it can be usefully applied in the CC context to discover undesired data dependencies between concurrent processes.

• Type: Conference
• Year: 1995
• Where: AGP
• Authors: Enea Zaffanella
• Keywords: AGP 1995, Artificial Intelligence, Downward Closed Observables, Reasonable Correctness Conditions, Static Analysis Framework