抽象化抽象机器：高阶程序分析的系统方法
摘要：预测模型对于构建可靠的软件系统至关重要。然而，对于现代高级编程语言而言，设计保守且可计算的程序行为近似（静态分析）仍然是一个困难且容易出错的过程。分析设计者需要的是一种精确的方法，来弥合语义与分析模型之间的差距：分析设计者需要一种能够驯服复杂语言特性（如高阶函数、递归、异常、延续、对象和动态分配）交互影响的方法。 我们提供了一种系统化的程序分析方法，能够产生新颖且透明的可靠静态分析。我们的方法依赖于现有的派生技术，将高级语言语义转化为低级确定性状态转换系统（具有潜在无限状态空间）。然后，我们进行一系列简单的机器重构，以获得一种可靠的、可计算的近似，该近似采用了具有有限状态空间的非确定性状态转换系统的形式。该方法可以统一扩展，以实现对包括高阶函数、尾调用、条件语句、副作用、异常、一级延续甚至垃圾回收在内的现实语言特性的程序分析。
作者：David Van Horn and Matthew Might
论文ID：1105.1743
分类：Programming Languages
分类简称：cs.PL
提交时间：2011-05-10