Using Symbolic Execution to Transform Turbo Abstract State Machines into Basic Abstract State Machines

This paper introduces a transformation method that uses symbolic execution to eliminate sequential composition ( \(\texttt {seq}\) ) rules from turbo ASM rules by translating them into equivalent rules without seq. Under some circumstances \(\texttt {iterate}\) rules can also be eliminated. The material presented here is work in progress. A prototype implementation of the transformation is publicly available.