# A Generic Approach to Symbolic Execution

3 DART - Contributions of the Data parallelism to real time
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
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.
Keywords :
Document type :
Reports
Domain :

https://hal.inria.fr/hal-00766220
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

### File

symbexec-techreport.pdf
Files produced by the author(s)

### Identifiers

• HAL Id : hal-00766220, version 2

### Citation

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

Record views