A Generic Framework for Symbolic Execution: ...
Type de document :
Compte-rendu et recension critique d'ouvrage
Titre :
A Generic Framework for Symbolic Execution: a Coinductive Approach
Auteur(s) :
Lucanu, Dorel [Auteur]
Department of Computer Science [Lasi]
Rusu, Vlad [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Arusoaie, Andrei [Auteur]
Department of Computer Science [Lasi]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Department of Computer Science [Lasi]
Rusu, Vlad [Auteur]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Arusoaie, Andrei [Auteur]
Department of Computer Science [Lasi]
Dynamic Reconfigurable Massively Parallel Architectures and Languages [DREAMPAL]
Titre de la revue :
Journal of Symbolic Computation
Pagination :
125-163
Éditeur :
Elsevier
Date de publication :
2017
ISSN :
0747-7171
Mot(s)-clé(s) en anglais :
formal operational semantics
circular coinduction
program verification
programming language
reachability logic
symbolic execution
circular coinduction
program verification
programming language
reachability logic
symbolic execution
Discipline(s) HAL :
Informatique [cs]/Logique en informatique [cs.LO]
Informatique [cs]/Langage de programmation [cs.PL]
Informatique [cs]/Langage de programmation [cs.PL]
Résumé en anglais : [en]
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 ...
Lire la suite >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.Lire moins >
Lire la suite >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.Lire moins >
Langue :
Anglais
Vulgarisation :
Non
Collections :
Source :
Fichiers
- https://hal.inria.fr/hal-01238696v2/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-01238696v2/document
- Accès libre
- Accéder au document
- https://hal.inria.fr/hal-01238696v2/document
- Accès libre
- Accéder au document
- document
- Accès libre
- Accéder au document
- JSC-PAS_2013_submission_10.pdf
- Accès libre
- Accéder au document