Verification by approximate forward and backward reachability

Approximate reachability techniques trade off accuracy for the capacity to deal with bigger designs. In this paper, we extend the idea of approximations using overlapping projections to symbolic backward reachability. This is combined with a previous method of computing overapproximate forward reachable state sets using overlapping projections. The algorithm computes a superset of the set of states that lie on a path from the initial state to a state that violates a specified invariant property. If this set is empty, there is no possibility of violating the invariant. If this set is non-empty, it may be possible to prove the existence of such a path by searching for a counter-example. A simple heuristic is given, which seems to work well in practice, for generating a counter-example path from this approximation. We evaluate these new algorithms by applying them to several control modules from the I/O unit in the Stanford FLASH Multiprocessor.