A Generic Framework for Symbolic Execution: a Coinductive Approach

Dorel Lucanu 1 Vlad Rusu 2 Andrei Arusoaie 1, 2
2 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. The approach is parameterised by a language definition, which consists of a signature for the lan-guage's syntax and execution infrastructure, a model interpreting the signature, and rewrite rules for the language's operational semantics. Then, symbolic execution amounts to computing symbolic paths using a derivative operation. We prove that the symbolic execution thus defined has the properties naturally expected from it, meaning that the feasible symbolic executions of a program and the concrete executions of the same program mutually simulate each other. We also show how a coinduction-based extension of symbolic execution can be used for the deductive verification of programs. We show how the proposed symbolic-execution approach, and the coinductive verification technique based on it, can be seamlessly implemented in language definition frameworks based on rewriting such as the K framework. A prototype implementation of our approach has been developed in K. We illustrate it on the symbolic analysis and deductive verification of nontrivial programs.
Type de document :
Article dans une revue
Journal of Symbolic Computation, Elsevier, 2017, 80, pp.125-163. 〈10.1016/j.jsc.2016.07.012〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01238696
Contributeur : Pal Dream <>
Soumis le : mercredi 6 janvier 2016 - 11:55:56
Dernière modification le : mardi 3 juillet 2018 - 11:26:09

Fichier

JSC-PAS_2013_submission_10.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Dorel Lucanu, Vlad Rusu, Andrei Arusoaie. A Generic Framework for Symbolic Execution: a Coinductive Approach. Journal of Symbolic Computation, Elsevier, 2017, 80, pp.125-163. 〈10.1016/j.jsc.2016.07.012〉. 〈hal-01238696v2〉

Partager

Métriques

Consultations de la notice

335

Téléchargements de fichiers

264