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
CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189, Inria Lille - Nord Europe
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 metadatas

Cited literature [46 references]  Display  Hide  Download

https://hal.inria.fr/hal-01238696
Contributor : Pal Dream <>
Submitted on : Wednesday, January 6, 2016 - 11:55:56 AM
Last modification on : Friday, March 22, 2019 - 1:34:44 AM

File

JSC-PAS_2013_submission_10.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

428

Files downloads

392