Formal Methods in Software Engineering

Using the Executable Semantics for CFG Extraction and Unfolding

Year2011
TypeConference
StatusPostproceedings
AuthorsMihail Asavoae, Irina Asavoae

Links

Abstract

The longest path search problem is particularly important in the context of low-level worst-case execution time analysis. This implies that all program executions are exhibited and inspected, via convenient abstractions, for their timing behavior. In this paper we present a definitional program unfolder, that is based on the formal executable semantics of a target language. We work with K, a rewrite-based framework for design and analysis of programming languages. Our methodology has two phases. First, it extracts, via reachability analysis, a safe control-flow graph (CFG) approximation, directly from the executable semantics of the language. Second, it unfolds the control-flow graph, annotated with loop bounds, and outputs the set of all possible program executions. The two-phased methodology describes, what we call, a definitional program unfolder and is implemented using the K-Maude tool, a prototype implementation of the K framework.

BibTeX

@inproceedings{aa-synasc11, author = {Mihail Asavoae and Irina Mariuca Asavoae}, title = {Using the Executable Semantics for CFG Extraction and Unfolding}, booktitle = {13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2011, Timisoara, Romania, September 26-29, 2011}, year = {2011}, pages = {123-127}, editor = {Dongming Wang and Viorel Negru and Tetsuo Ida and Tudor Jebelean and Dana Petcu and Stephen M. Watt and Daniela Zaharie}, publisher = {IEEE Computer Society}, isbn = {978-1-4673-0207-4}, url ={http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=6169511&url=http%3A%2F%2Fieeexplore.ieee.org%2Fxpls%2Fabs_all.jsp%3Farnumber%3D6169511[aa-synasc11]} }