en fr A Generic Framework for Symbolic Execution: Theory and Applications Un cadre générique pour lexécution symbolique : théorie et applications Reportar como inadecuado




en fr A Generic Framework for Symbolic Execution: Theory and Applications Un cadre générique pour lexécution symbolique : théorie et applications - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 Department of Compter Science 2 Department of Computer Science Lasi 3 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille - 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 language-s syntax and execution infrastructure, a model interpreting the signature, and rewrite rules for the language-s operational semantics. Then, symbolic execution amounts to performing a so-called symbolic rewriting, which consists in changing both the model and the manner in which the operational semantics rules are applied. We prove that the symbolic execution thus defined has the properties naturally expected from it. A prototype implementation of our approach was developed in the K Framework. We demonstrate the genericity of our tool by instantiating it on several languages, and show how it can be used for the symbolic execution, bounded model checking, and deductive verification of several programs.

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 revientalors à 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é notreapproche 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.

Keywords : Program Verification Symbolic Execution K framework





Autor: Andrei Arusoaie - Dorel Lucanu - Vlad Rusu -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados