Abstracting abstract machines
Abstracting abstract machines
复制标题
抽象抽象机器
DOI：
10.1145/1995376.1995400
复制
发表时间：
2011
影响因子：
22.7
通讯作者：
M. Might
中科院分区：
文献类型：
--
作者：
David Van Horn;M. Might
预测模型是工程可靠的软件系统的基础。但是，对于计划的行为（静态分析）设计保守的，可计算的近似值仍然是现代高级编程语言的困难且容易出错的过程。分析设计师需要的是一种用于导航语义和分析模型之间差距的原则方法：分析设计人员需要一种驯服复杂语言特征（例如高阶功能，递归，递归，异常，连续性，对象和动态分配）的方法。我们为程序分析提供了系统的方法，该方法可以产生新颖且透明的静态分析。我们的方法依赖于现有的衍生技术来将高级语言语义转化为低级确定性国家转变系统（具有潜在的无限状态空间）。然后，我们执行一系列简单的机器重构以获得声音，可计算的近似值，该近似以有限状态空间采用非确定性状态转换系统的形式。该方法统一扩展，以启用现实语言特征的程序分析，包括高阶功能，尾部呼叫，条件，副作用，例外，一流的连续性，甚至垃圾收集。
Predictive models are fundamental to engineering reliable software systems. However, designing conservative, computable approximations for the behavior of programs (static analyses) remains a difficult and error-prone process for modern high-level programming languages. What analysis designers need is a principled method for navigating the gap between semantics and analytic models: analysis designers need a method that tames the interaction of complex languages features such as higher-order functions, recursion, exceptions, continuations, objects and dynamic allocation. We contribute a systematic approach to program analysis that yields novel and transparently sound static analyses. Our approach relies on existing derivational techniques to transform high-level language semantics into low-level deterministic state-transition systems (with potentially infinite state spaces). We then perform a series of simple machine refactorings to obtain a sound, computable approximation, which takes the form of a non-deterministic state-transition systems with finite state spaces. The approach scales up uniformly to enable program analysis of realistic language features, including higher-order functions, tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection.