A Generic Approach to Symbolic Execution - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2012

A Generic Approach to Symbolic Execution

Résumé

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.
Nous proposons un cadre général pour l'exécution symbolique de programmes écrits dans des langages munis de sémantiques formelles définies par réécriture de termes. Partant de la définition \ d'un langage, on construit automatiquement la définition d'un nouveau langage qui a la même syntaxe que l'original, mais dont les types de données sont étendus avec des valeurs symboliques, et dont les régles sémantiques sont transformées afin de traiter les valeurs symboliques. L'exécution symbolique des programmes du langage d'origine est alors définie comme l'exécution habituelle des programmes du langage transformé. Nous démontrons que l'exécution symbolique posséde les propriétés attendues par rapport á l'exécution concréte. Nous avons implémenté notre approche dans un outil prototype dans la \emph{K framework}. L'aspect générique de l'outil est mis en évidence par son instanciation sur plusieurs langages. Nous montrons enfin comment l'outil permet l'exécution symbolique et le \emph{model checking} de programmes.
Fichier principal
Vignette du fichier
symbexec-techreport.pdf (1.06 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-00766220 , version 1 (17-12-2012)
hal-00766220 , version 2 (20-12-2012)
hal-00766220 , version 3 (21-06-2013)
hal-00766220 , version 4 (15-03-2014)
hal-00766220 , version 5 (21-03-2014)
hal-00766220 , version 6 (06-04-2014)
hal-00766220 , version 7 (01-09-2015)
hal-00766220 , version 8 (03-09-2015)

Identifiants

  • HAL Id : hal-00766220 , version 3

Citer

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

Partager

Gmail Facebook X LinkedIn More