Symbolic execution for a clash-free subset of ASMs.

Providing efficient theorem proving support for general ASM rules that update proper functions, use sequential and parallel composition, nondeterministic choice and recursion is difficult, since it is not easy to find a predicate logic formula that describes the transition relation of an ASM rule. One important obstacle to achieving this goal is that executing rules may result in a clash, that aborts the ASM run. This paper contributes three results towards this goal.