Abstract: Generalized Symbolic trajectory evaluation is a powerful model checking technique which introduces symbolic quaternary and symbolic variables into symbolic quaternary assignments. But to find Counter-example has obstacles. In this paper, we presented an solution to search Counter-example. It uses set Intersection to backward simulation to generalized Counter-example. And we extended the solution to solve the problems from symbolic variable.

Key words: Generalized symbolic trajectory evaluation,Counter-example,Formal verification,Symbolic model-checking,Abstraction