A Generic Framework for 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 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 L, a new definition Lsym is automatically generated, which has the same syntax, but whose semantics extends L's data domains with symbolic values and adapts the semantical rules of L to deal with the new domains. Then, the symbolic execution of Lprograms is the concrete execution of the corresponding Lsym programs, i.e., the application of the rewrite rules in the semantics of Lsym. 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 K framework. A prototype symbolic execution engine also written in K is presented.
Type de document :
Communication dans un congrès
Erwig, M. and Paige, R.F. and Van Wyk, E. 6th International Conference on Software Language Engineering, Oct 2013, Indianapolis, United States. Springer Verlag, LNCS 8225, pp.281-301, 2013, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00853588
Contributeur : Mister Dart <>
Soumis le : jeudi 22 août 2013 - 22:42:57
Dernière modification le : jeudi 11 janvier 2018 - 06:25:37
Document(s) archivé(s) le : jeudi 6 avril 2017 - 05:10:13

Fichier

sle2013.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00853588, version 1

Collections

Citation

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu. A Generic Framework for Symbolic Execution. Erwig, M. and Paige, R.F. and Van Wyk, E. 6th International Conference on Software Language Engineering, Oct 2013, Indianapolis, United States. Springer Verlag, LNCS 8225, pp.281-301, 2013, Lecture Notes in Computer Science. 〈hal-00853588〉

Partager

Métriques

Consultations de la notice

509

Téléchargements de fichiers

289