Accéder directement au contenu Accéder directement à la navigation

Specification of Concretization and Symbolization Policies in Symbolic Execution

Abstract : Symbolic Execution (SE) is a popular and profitable approach to automatic code-based software testing. Concretization and symbolization (C/S) is a crucial part of modern SE tools, since it directly impacts the trade-offs between correctness, completeness and efficiency of the approach. Yet, C/S policies have been barely studied. We intend to remedy to this situation and to establish C/S policies on a firm ground. To this end, we propose a clear separation of concerns between C/S specification on one side, through the new rule-based description language CSml, and the algorithmic core of SE on the other side, revisited to take C/S policies into account. This view is implemented on top of an existing SE tool, demonstrating the feasibility and the benefits of the method. This work paves the way for more flexible SE tools with well-documented and reusable C/S policies, as well as for a systematic study of C/S policies.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

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

http://hal.univ-grenoble-alpes.fr/hal-01721492
Contributeur : Laurent Mounier <>
Soumis le : vendredi 2 mars 2018 - 11:06:54
Dernière modification le : lundi 30 mars 2020 - 13:48:46
Document(s) archivé(s) le : jeudi 31 mai 2018 - 14:56:37

Fichier

issta-2016.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01721492, version 1

Citation

Robin David, Sébastien Bardin, Josselin Feist, Laurent Mounier, Marie-Laure Potet, et al.. Specification of Concretization and Symbolization Policies in Symbolic Execution. ISSTA 2016 - The International Symposium on Software Testing and Analysis , Jul 2016, Saarland, Germany. pp.1-11. ⟨hal-01721492⟩

Partager

Métriques

Consultations de la notice

708

Téléchargements de fichiers

252