Rewriting for Symbolic Execution of State Machine Models

We describe an algorithm for simplifying a class of symbolic expressions that arises in the symbolic execution of formal state machine models. These expressions are compositions of state access and change functions and if-then-else expressions, laced together with local variable bindings (e.g., lambda applications). The algorithm may be used in a stand-alone way, but is designed to be part of a larger system employing a mix of other strategies. The algorithm generalizes to a rewriting algorithm that can be characterized as outside-in or lazy, with respect both to variable instantiation and equality replacement. The algorithm exploits memoization or caching.