Formal Methods in Software Engineering

Symbolic execution based on language transformation

Year2015
TypeJournal
StatusPublished
AuthorsAndrei Arusoaie, Dorel Lucanu, Vlad Rusu

Links

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. 

BibTeX

@Article{Arusoaie201548, author = {Andrei Arusoaie and Dorel Lucanu and Vlad Rusu}, title = {Symbolic execution based on language transformation }, journal = {Computer Languages, Systems & Structures }, volume = {44, Part A}, pages = {48 - 71}, year = {2015}, note = {Special issue on the 6th and 7th International Conference on Software Language Engineering ({SLE} 2013 and {SLE} 2014) }, issn = {1477-8424}, url = {http://dx.doi.org/10.1016/j.cl.2015.08.004 [DOI]}, publisher = {Elsevier}, url_publisher = {http://www.sciencedirect.com/science/article/pii/S147784241500055X} }