Using the Executable Semantics for CFG Extraction and Unfolding

被引：0

作者：

Asavoae, Mihail ^{[1
]}

Asavoae, Irina Mariuca ^{[1
]}

机构：

[1] Alexandru Ioan Cuza Univ, Fac Comp Sci, Iasi, Romania

来源：

13TH INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2011) | 2012年

关键词：

D O I：

10.1109/SYNASC.2011.53

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The longest path search problem is important in low-level worst-case execution time analysis and 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 the design and analysis of programming languages. Our methodology has two phases. First, it extracts directly from the executable semantics of the language, via reachability analysis, a safe control-flow graph (CFG) approximation. Second, it unfolds the control-flow graph, using loop bounds annotations and outputs the set of all possible program executions. The two-phased definitional program unfolder is implemented using the K-Maude tool, a prototype implementation of the K framework.

引用

页码：123 / 127

页数：5

共 15 条

[1]

Asavoae M., 2011, WCET

[2]

BALAKRISHNAN G, 2004, 200, P5

[3]

Clavel Manuel., 2007, All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, V4350

[4]

Ellison C., 2010, TECH REP

[5]

Esparza J., 1996, Tools and Algorithms for the Construction and Analysis of Systems. Second International Workshop, TACAS '96. Proceedings, P87

[6] Generic control flow reconstruction from assembly code [J].

Kästner, D ;

Wilhelm, S .

ACM SIGPLAN NOTICES, 2002, 37 (07) :46-55

[7]

Kinder J, 2009, LECT NOTES COMPUT SC, V5403, P214, DOI 10.1007/978-3-540-93900-9_19

[8]

Li YTS, 1995, IEEE REAL TIME, P298, DOI 10.1109/REAL.1995.495219

[9]

Meredith Patrick, 2010, 2010 8th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), P179, DOI 10.1109/MEMCOD.2010.5558634

[10]

Rosu G., 2010, LNCS

← 1 2 →