Path Directed Symbolic Execution in the K Framework

The K framework is a rewrite-based executable semantic framework built with the purpose to define programming languages and formal analysis methods. This paper introduces K definition of the path-directed symbolic execution, which is that part of Counterexample Guided Abstraction Refinement (CEGAR) where the counterexample is checked for spuriousness. To express this technique in K, we use strongest post condition computation on straight line code. The programming language at hand is imperative, with simple arithmetic, but the approach can be applied to more complicated languages. This work aims to further advance the integration of CEGAR technique in rewriting logic semantics project in general, and in K in particular. By doing this we obtain an uniform description of the definition of the programming language, the abstract model checking, and the counterexample guided refinement. This uniformity enables formal reasoning about CEGAR´s implementation correctness which could be further standardized and eventually automatized.