Skip to Main content Skip to Navigation
Journal articles

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 - 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.
Complete list of metadata

Cited literature [46 references]  Display  Hide  Download
Contributor : Pal Dream Connect in order to contact the contributor
Submitted on : Wednesday, January 6, 2016 - 11:55:56 AM
Last modification on : Friday, January 7, 2022 - 3:43:58 AM


Files produced by the author(s)



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⟩



Les métriques sont temporairement indisponibles