Verification by approximate forward and backward reachability
Shankar G. Govindaraju, David L. Dill · 1998
Approximate reachability techniques trade off accuracy for the capacity to deal with bigger desigw.In this paper, we extend the idea of approximations using overlapping projection to symbolic backward reachability.Thti is combined with a previous method of computing ouerapprom.mateforward reachable state sets using overlapping projections.The algom"thmcomputes a superset of the set of states that lie on a path from the initial state to a state that violates a specified invan.antproperty.If this set h empty, there ti no possibility of violating the invan.ant.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 appron.mation.JVe evaluate these new algom.thmsby applying them to several control modules porn the I/O unit in the Stanford FLASH J!ultiprocessor.