Symbolic Execution in the K Framework: Support and Applications

K (www.kframework.org) is an executable semantic framework for defining operational semantics of programming languages, type systems, and formal analysis tools. The K toolbox includes two main tools: the compiler and the runner. The K definition of a language, say, L, is compiled into a rewrite system. Then, the K runner executes programs in L by applying the resulting rewrite rules to configurations containing programs. Beside some simple languages used for teaching, there are a few real-word programming languages, supporting different paradigms, that have been successfully defined in K: C, Python, Java, OCaml. In [1] a symbolic execution language-independent framework is defined and a prototype of this is implemented in K. This implementation extends the K compiler with a new feature that builds a “symbolic semantics” of the language, which is able to execute programs having symbolic values as inputs. The new semantics is automatically generated from the initial K definition of the language by reusing components of the K framework: parsing, compilation steps, support for symbolic execution, and the connections to the Maude’s model-checker and the Z3 SMT solver. The result of the symbolic execution consists in a set of logical constrained configurations corresponding to different program paths. In this talk we briefly present the K framework, its symbolic execution support and how the symbolic execution is used for program analysis. In particular, we show how the existing analysis tools (e.g., the model-checker) can be used together with the symbolic semantics and how the symbolic exception mechanism can be extended to verify properties expressed as Reachability Logic formulas [2].

References

1. A. Arusoaie, D. Lucanu, and V. Rusu. A generic framework for symbolic execution. In 6th International Conference on Software Language Engineering, volume 8225 of LNCS, pages 281–301. Springer Verlag, 2013. Also available as a technical report at http://hal.inria.fr/hal-00766220/.

2. A. Arusoaie, D. Lucanu, and V. Rusu. Language-Independent Program Verification Using Symbolic Execution. Rapport de recherche RR-8369, INRIA, Sept. 2013. http://hal.inria.fr/hal-00864341/.

Sidebar