Optimizing Abstract Abstract Machines

被引：0

作者：

Johnson, J. Ian ^{[1
]}

Labich, Nicholas ^{[1
]}

Might, Matthew ^{[2
]}

Van Horn, David ^{[1
]}

机构：

[1] Northeastern Univ, Boston, MA 02115 USA

[2] Univ Utah, Salt Lake City, UT 84112 USA

来源：

ACM SIGPLAN NOTICES | 2013年 / 48卷 / 09期

关键词：

abstract machines; abstract interpretation;

D O I：

10.1145/2544174.2500604

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The technique of abstracting abstract machines (AAM) provides a systematic approach for deriving computable approximations of evaluators that are easily proved sound. This article contributes a complementary step-by-step process for subsequently going from a naive analyzer derived under the AAM approach, to an efficient and correct implementation. The end result of the process is a two to three order-of-magnitude improvement over the systematically derived analyzer, making it competitive with hand-optimized implementations that compute fundamentally less precise results.

引用

页码：443 / 454

页数：12

共 34 条

[1]

Boucher D., 1996, Compiler Construction. 6th International Conference, CC'96. Proceedings, P192

[2]

BRAVENBOER M, 2009, OOPSLA 09

[3] CHARACTERIZING FINITE KRIPKE STRUCTURES IN PROPOSITIONAL TEMPORAL LOGIC [J].

BROWNE, MC ;

CLARKE, EM ;

GRUMBERG, O .

THEORETICAL COMPUTER SCIENCE, 1988, 59 (1-2) :115-131

[4]

Chailloux Emmanuel, 1996, J FUNCT PROGRAM, V6, P621, DOI [10.1017/S0956796800001891, DOI 10.1017/S0956796800001891]

[5]

Cousot P., 1979, POPL, P269, DOI [10.1145/567752.567778, DOI 10.1145/567752.567778]

[6]

Cousot Patrick, 1977, POPL, DOI DOI 10.1145/512950.512973

[7]

D'Osualdo E., 2012, TECHNICAL REPORT

[8]

Danvy Olivier, 2004, RS0426 BRICS AARH U

[9]

Danvy Olivier, 2006, THESIS AARHUS U

[10] Introspective Pushdown Analysis of Higher-Order Programs [J].

Earl, Christopher ;

Sergey, Ilya ;

Might, Matthew ;

Van Horn, David .

ACM SIGPLAN NOTICES, 2012, 47 (09) :177-188

← 1 2 3 4 →