Symbolic execution based on language transformation. (December 2015)

• Record Type: Journal Article
• Authors: Arusoaie, Andrei; Lucanu, Dorel; Rusu, Vlad
• Is Part Of: Computer languages, systems & structures. Volume 44:Part A(2015)
• Page Start: 48
• Page End: 71
• Publication Date: 2015-12
• Subjects: Symbolic execution -- Formal semantics -- Programming languages -- Program analysis; Programming languages (Electronic computers) -- Periodicals; Computer networks -- Periodicals; Computer architecture -- Periodicals; Computer systems -- Periodicals; Langage de programmation; Réseau d'ordinateurs; Architecture d'ordinateur; Périodique électronique (Descripteur de forme); Ressource Internet (Descripteur de forme); 005.13
• DOI: 10.1016/j.cl.2015.08.004
• Languages: English
• ISSNs: 1477-8424

Abstract

Abstract: We propose a language-independent symbolic execution framework for languages endowed with a formal operational semantics based on term rewriting. Starting from a given definition of a language, a new language definition is generated, with the same syntax as the original one, but whose semantical rules are transformed in order to rewrite over logical formulas denoting possibly infinite sets of program states. Then, the symbolic execution of concrete programs is, by definition, the execution of the same programs with the symbolic semantics. We prove that the symbolic execution thus defined has the properties naturally expected from it (with respect to concrete program execution). A prototype implementation of our approach was developed in the K framework. We demonstrate the tool׳s genericity by instantiating it on several languages, and illustrate it on the reachability analysis and model checking of several programs. Abstract : Highlights: We propose a language-independent symbolic execution framework for languages. The proposed language-independent approach is based on language transformations. We prove that the expected formal properties of symbolic execution. We present a prototype and we use it on several languages.