Sciweavers

CP
2009
Springer

An Interpolation Method for CLP Traversal

14 years 4 months ago
An Interpolation Method for CLP Traversal
We consider the problem of exploring the search tree of a CLP goal in pursuit of a target property. Essential to such a process is a method of tabling to prevent duplicate exploration. Typically, only actually traversed goals are memoed in the table. In this paper we present a method where, upon the successful traversal of a subgoal, a generalization of the subgoal is memoed. This enlarges the record of already traversed goals, thus providing more pruning in the subsequent search process. The key feature is that the abstraction computed is guaranteed not to give rise to a spurious path that might violate the target property. A driving application area is the use of CLP to model the behavior of other programs. We demonstrate the performance of our method on a benchmark of program verfication problems.
Joxan Jaffar, Andrew E. Santosa, Razvan Voicu
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where CP
Authors Joxan Jaffar, Andrew E. Santosa, Razvan Voicu
Comments (0)