Symbolic execution for a clash-free subset of ASMs

Third, we show that the relational encoding can be used to justify a calculus for clash-free ASM rules based on symbolic execution. Such a calculus is useful for interactive theorem provers such as our tool KIV.