A Generic Approach to Symbolic Execution
Andrei Arusoaie, Dorel Lucanu, Vlad Rusu · 2012
We propose a generic, language-independent symbolic execution approach for languages endowed with a formal operational semantics based on term rewriting. Starting from the definition of a language $\cal L$, a new definition ${\cal L}^{\it sym}$ is automatically generated, which has the same syntax, but whose semantics extends ${\cal L}$'s data domains with symbolic values and adapts the semantical rules of $\cal L$ to deal with the new domains. Then, the symbolic execution of ${\cal L}$ programs is the concrete execution of the corresponding ${\cal L}^{\it sym}$ programs, i.e., the application of the rewrite rules in the semantics of ${\cal L}^{\it sym}$. We prove that the symbolic execution thus defined has the adequate properties normally expected from it, and illustrate the approach on a simple imperative language defined in the $\mathbb{\K}$ framework. A prototype symbolic execution engine also written in $\mathbb{\K}$ is presented.