Symbolic execution for a clash-free subset of ASMs

• Published in: Science of computer programming 2018-06, Vol.158, p.21-40
• Main Authors: Schellhorn, Gerhard, Ernst, Gidon, Pfähler, Jörg, Bodenmüller, Stefan, Reif, Wolfgang
• Format: Article
• Language: English
• Subjects: Abstract state machines; Clashes; Symbolic execution; Synchronous parallelism
• ISSN: 0167-6423; 1872-7964
• DOI: 10.1016/j.scico.2017.08.014

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. •Static check for clash-freedom of ASM rules with nondeterminism and recursion.•Relational encoding for ASM rules that satisfy the status check.•Calculus with symbolic execution rules based on the relational encoding.