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 fra\-mework. The approach is parameterised by a language definition, which consists of a signature for the language's syntax and execution infrastructure, a model interpreting the signature, and rewrite rules for the language's operational semantics. Then, symbolic execution amounts to performing a so-called symbolic rewriting, which consists in changing both the model and the manner in which the operational semantics rules are applied. 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 :
Complete list of metadatas

Contributor : Mister Dart <>
Submitted on : Saturday, March 15, 2014 - 2:44:10 PM
Last modification on : Thursday, February 21, 2019 - 10:34:09 AM
Long-term archiving on: Monday, April 10, 2017 - 12:10:33 AM


Files produced by the author(s)


  • HAL Id : hal-00766220, version 4


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



Record views


Files downloads