A Generic Framework for Symbolic Execution
Type de document :
Communication dans un congrès avec actes
Titre :
A Generic Framework for Symbolic Execution
Auteur(s) :
Arusoaie, Andrei [Auteur]
Lucanu, Dorel [Auteur]
Department of Computer Science [Lasi]
Rusu, Vlad [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Lucanu, Dorel [Auteur]
Department of Computer Science [Lasi]
Rusu, Vlad [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Éditeur(s) ou directeur(s) scientifique(s) :
Erwig
M. and Paige
R.F. and Van Wyk
E.
M. and Paige
R.F. and Van Wyk
E.
Titre de la manifestation scientifique :
6th International Conference on Software Language Engineering
Ville :
Indianapolis
Pays :
Etats-Unis d'Amérique
Date de début de la manifestation scientifique :
2013-10-27
Titre de la revue :
Lecture Notes in Computer Science
Éditeur :
Springer Verlag
Date de publication :
2013-08
Discipline(s) HAL :
Informatique [cs]/Systèmes embarqués
Résumé en anglais : [en]
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 ...
Lire la suite >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.Lire moins >
Lire la suite >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.Lire moins >
Langue :
Anglais
Comité de lecture :
Oui
Audience :
Internationale
Vulgarisation :
Non
Collections :
Source :
Fichiers
- https://hal.inria.fr/hal-00853588/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-00853588/document
- Accès libre
- Accéder au document
- document
- Accès libre
- Accéder au document
- sle2013.pdf
- Accès libre
- Accéder au document