An Interpolation Method for State Space Exploration

Joxan Jaffar, Andrew Santosa and Razvan Voicu

Abstract

We consider the problem of state-space exploration of a symbolic computation tree in pursuit of a target property. Essential to such exploration is memoing to prevent duplicate exploration. Typically, only actually traversed states are memoed. In this paper we present a method where, upon the successful traversal of a state, a {\em superset} or abstraction of this state is memoed. This enlarges the record of already traversed states, thus providing 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 violates the target property.