抽象化抽象机
摘要：基于派生的方法进行抽象解释：具有透明度和可靠性的静态分析 将派生方法应用于成熟的抽象机器，我们提出了一种基于派生的抽象解释方法，并产生了新颖且透明可靠的静态分析。为了证明该技术并支持我们的主张，我们将Felleisen和Friedman的CEK机器（一种Krivine机器的延迟变种）以及Clements和Felleisen的堆栈检查CM机器转化为它们自身的抽象解释。得到的分析结果有以下特点：限制程序事件的时间顺序；预测返回流和堆栈检查行为；近似处理按需参数的流和计算。对于所有这些机器，我们发现一系列众所周知的具体机器重构，加上我们称之为存储分配的延续技术，会导致机器被简单地限制在静态分析中通过其存储区间。我们证明了这种技术的规模效应一致，允许对现实语言特性进行静态分析，包括尾调用、条件语句、副作用、异常、第一类延续甚至垃圾收集。
作者：David Van Horn and Matthew Might
论文ID：1007.4446
分类：Programming Languages
分类简称：cs.PL
提交时间：2010-09-09