Name
Abstract | ||
|---|---|---|
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.
|
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-04244-7_37 | Principles and Practice of Constraint Programming |
Keywords | Field | DocType |
program verfication problem,traversed goal,abstraction computed,search tree,target property,interpolation method,key feature,duplicate exploration,subsequent search process,clp traversal,clp goal,driving application area | Mathematical optimization,Tree traversal,Abstraction,Computer science,Interpolation,Algorithm,Theoretical computer science,Constraint logic programming,Spurious relationship,Search tree | Conference |
Volume | ISSN | ISBN |
5732 | 0302-9743 | 3-642-04243-0 |
Citations | PageRank | References |
30 | 1.01 | 25 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Joxan Jaffar | 1 | 2350 | 283.50 |
| Andrew Santosa | 2 | 146 | 13.36 |
| Razvan Voicu | 3 | 57 | 4.22 |