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
Résumé : Nous proposons un cadre général pour l’exécution symbolique de programmes, qui est indépendant des langages dans lesquels les programmes en question sont écrits. L’approche est paramétrisée par une définition de langage, qui consiste en une signature pour la syntaxe du langage et pour son infrastructure, un modèle interprétant la signature, et un ensemble de règles de réécriture définissant la sémantique opérationnelle du langage. L’exécution symbolique revient alors à modifier calculer des chemins symboliques en utilisant une opration dite de dérivation. Nous démontrons que l’exécution symbolique possède les propriétés attendues par rapport à l’exécution concrète: les exécutions symboliques et concrètes d’un même programme se simulent mutuellement. Nous montrons également qu’une extension coinductive de l’exécution symbolique peut être utilisée pour la vérification déductive de programmes. Nous avons implémenté notre approche dans un outil prototype dans la 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’analyse symbolique, le model checking borné, et la vérification déductive de programmes.
Type de document :
Rapport
[Research Report] RR-8189, Inria. 2015, pp.41
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00766220
Contributeur : Mister Dart <>
Soumis le : jeudi 3 septembre 2015 - 11:44:53
Dernière modification le : mardi 3 juillet 2018 - 11:48:06
Document(s) archivé(s) le : mercredi 26 avril 2017 - 14:46:08

Fichier

jsc2014-techreport.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

292

Téléchargements de fichiers

252