A Generic Approach to Symbolic Execution

Abstract : 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.
Document type :
Complete list of metadatas

Contributor : Mister Dart <>
Submitted on : Thursday, December 20, 2012 - 2:56:02 PM
Last modification on : Thursday, February 21, 2019 - 10:52:49 AM
Long-term archiving on : Sunday, December 18, 2016 - 7:24:31 AM


Files produced by the author(s)


  • HAL Id : hal-00766220, version 2


Andrei Arusoaie, Dorel Lucanu, Vlad Rusu. A Generic Approach to Symbolic Execution. [Research Report] RR-8189, 2012, pp.21. ⟨hal-00766220v2⟩



Record views


Files downloads