A Generic Approach to Symbolic Execution

Andrei Arusoaie 1 Dorel Lucanu 2 Vlad Rusu 3
3 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Université de Lille, Sciences et Technologies, Inria Lille - Nord Europe, CNRS - Centre National de la Recherche Scientifique
Abstract : We propose a language-independent symbolic execution framework for languages endowed with a formal operational semantics based on term rewriting. Starting from a given definition of a language, a new language definition is automatically generated, which has the same syntax as the original one but whose semantics extends data domains with symbolic values and adapts semantical rules to deal with these values. Then, the symbolic execution of concrete programs is the execution of programs with the new symbolic semantics, on symbolic input data. We prove that the symbolic execution thus defined has the properties naturally expected from it. A prototype implementation of our approach was developed in the K Framework. We demonstrate the genericity of our tool by instantiating it on several languages, and show how it can be used for the symbolic execution and model checking of several programs.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/hal-00766220
Contributor : Mister Dart <>
Submitted on : Friday, June 21, 2013 - 5:25:39 PM
Last modification on : Thursday, February 21, 2019 - 10:34:09 AM
Long-term archiving on : Wednesday, April 5, 2017 - 1:57:48 AM

File

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

Identifiers

  • HAL Id : hal-00766220, version 3

Citation

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

Share

Metrics

Record views

231

Files downloads

261