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 :
Reports
Complete list of metadatas

https://hal.inria.fr/hal-00766220
Contributor : Mister Dart <>
Submitted on : Monday, December 17, 2012 - 7:09:24 PM
Last modification on : Thursday, February 21, 2019 - 10:52:49 AM
Long-term archiving on : Sunday, December 18, 2016 - 3:41:43 AM

File

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

Identifiers

  • HAL Id : hal-00766220, version 1

Citation

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

Share

Metrics

Record views

32

Files downloads

52