A Generic Framework for Symbolic Execution: Theory and Applications

Andrei Arusoaie 1 Dorel Lucanu 2 Vlad Rusu 3
3 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
Abstract : We propose a language-independent symbolic execution framework. 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, bounded model checking, and deductive verification of several programs.
Liste complète des métadonnées

Cited literature [48 references]  Display  Hide  Download

https://hal.inria.fr/hal-00766220
Contributor : Mister Dart <>
Submitted on : Thursday, September 3, 2015 - 11:44:53 AM
Last modification on : Wednesday, July 25, 2018 - 1:23:07 AM
Document(s) archivé(s) le : Wednesday, April 26, 2017 - 2:46:08 PM

File

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

Identifiers

  • HAL Id : hal-00766220, version 8

Citation

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu. A Generic Framework for Symbolic Execution: Theory and Applications. [Research Report] RR-8189, Inria. 2015, pp.41. 〈hal-00766220v8〉

Share

Metrics

Record views

335

Files downloads

276