A generic framework for symbolic execution: A coinductive approach. (May 2017)

• Record Type: Journal Article
• Authors: Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei
• Is Part Of: Journal of symbolic computation. Volume 80:Part 1(2017)
• Page Start: 125
• Page End: 163
• Publication Date: 2017-05
• Subjects: Symbolic execution -- Programming language -- Formal operational semantics -- Reachability logic -- Circular coinduction -- Program verification; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2016.07.012
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: We propose a language-independent symbolic execution framework. The approach is parameterised by a language definition, which consists of a signature for the syntax and execution infrastructure of the language, 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.