Symbolic execution based on language transformation

Andrei Arusoaie 1 Dorel Lucanu 2 Vlad Rusu 1
1 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
Abstract : 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 generated, with the same syntax as the original one, but whose semantical rules are transformed in order to rewrite over logical formulas denoting possibly infinite sets of program states. Then, the symbolic execution of concrete programs is, by definition , the execution of the same programs with the symbolic semantics. We prove that the symbolic execution thus defined has the properties naturally expected from it (with respect to concrete program execution). A prototype implementation of our approach was developed in the K Framework. We demonstrate the tool's genericity by instantiating it on several languages, and illustrate it on the reachability analysis and model checking of several programs.
Type de document :
Article dans une revue
Computer Languages, Systems and Structures, Elsevier, 2015, pp.42. 〈10.1016/j.cl.2015.08.004〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01186008
Contributeur : Pal Dream <>
Soumis le : dimanche 23 août 2015 - 11:46:35
Dernière modification le : mardi 3 juillet 2018 - 11:33:58
Document(s) archivé(s) le : mercredi 26 avril 2017 - 10:18:55

Fichier

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

Identifiants

Collections

Citation

Andrei Arusoaie, Dorel Lucanu, Vlad Rusu. Symbolic execution based on language transformation. Computer Languages, Systems and Structures, Elsevier, 2015, pp.42. 〈10.1016/j.cl.2015.08.004〉. 〈hal-01186008〉

Partager

Métriques

Consultations de la notice

310

Téléchargements de fichiers

157