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. First, it shows that it is possible to compute a first-order formula for each rule that implies clash-freedom when provable. The derived formula is not a precise characterization, but is provable for many ASMs that are used in practice. Second, we give axioms that describe the transition relation for clash-free ASM rules as formulas of predicate logic that can be used to verify pre/post-condition assertions using automated theorem provers. 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.
published 2017 Science of Computer Programming

Publisher: Elsevier

DOI: j.scico.2017.08.014

For questions regarding the publication, please contact!