Backward Symbolic Execution of Protocols.
Gerard J. Holzmann · 1984
A traditional method to validate protocols by state space exploration is to use forward symbolic execution. One of the main problems of this approach is that to find all undesirable system states one has to generate all reachable states and evaluate all desirable system states as well. The paper discusses an alternative search strategy based on backward symbolic execution. This time we start with a state that we know to be undesirable and execute the protocol backwards, evaluating only undesirable states in an effort to show that they are unreachable.