ACM通信

研究突出了

技术角度:抽象抽象机器

奥利维尔·丹维，简·米德加德
ACM通讯，2011年9月，54卷9号，100页
10.1145/1995376.1995399
评论

程序分析的目标是在不运行程序的情况下静态地预测程序的运行时属性。程序分析的语义方法起源于Cousot对抽象解释的开创性工作:从程序执行的正式数学模型开始语义然后用伽罗瓦连接(或类似的方法)将其近似化为一个基于运行时属性格的可计算模型，该模型考虑了所有可能的执行路径。每个程序产生一系列方程，然后典型地通过不动点迭代来解决。

因此，基于语义的程序分析需要(1)从“友好的”语义开始;设计一个“相宜”的运行时属性格;(3)将一组“相关”方程与程序相关联;(4)有效地解出这些方程。

每一项要求都充满了困难:

1. 在存在的各种形式语义(操作的、指称的、公理的，等等)及其子语义(例如，小步骤或大步骤)中，您的友好语义在哪里?理想情况下，它应该使自己很好地近似成一个可计算的模型。
2. 什么是运行时性质的相合晶格?它应该有多宽?有多高?理想情况下，它应该是一种很好的扩展算子，可以在不影响结果精度的前提下加速不动点迭代的收敛。
3. 什么是相关的方程组?理想情况下，每个方程应该尽可能地模仿友好的语义。
4. 方程的最佳表示和最有效的解决方法是什么?这是一个算法问题。

这些问题的有效答案以前就已经找到了，但似乎每一个都是绝招。

在下面的论文中，大卫·范霍恩和马修·梅特对简单和有效进行了彻底的押注:

• 由于大多数语义工件是可互导的，没有失去一般性，它们选择抽象机器确定性状态转换系统，潜在无限状态空间作为友好的语义。
• 然后，他们将每个抽象机器重构为一个具有有限状态空间的非确定性状态转换系统。

---

我们发现Van Horn和Might的科学贡献是如何通过抽象机器来开发高阶程序分析的有效教程。

---

他们的方法非常有用:它使程序分析设计人员能够从现有的抽象机器开始，而不是从专门的、量身定做的机器开始，然后将其统一地分解为抽象友好的语义工件。他们的方法是有效的:它可以扩展到各种计算情况，包括实际的编程语言构造，例如异常。他们的方法是结构化的和通用的:它使程序分析设计师专注于他们的分析的具体内容，这仍然是困难的——他们的运行时属性格，他们的扩展操作符，如何表示他们的方程，以及如何有效地解决它们，而不是被迫执行一个又一个全球性的绝招，从头开始，每一次。

因此，我们发现Van Horn和Might的科学贡献在概念和实践上是一个重要的垫脚石，同时也是如何通过抽象机器来开发高阶程序分析的有效教程。我们也发现他们的文章读起来很有趣。

回到顶部

数字图书馆是由计算机协会出版的。版权所有©2011 ACM股份有限公司

---

没有发现记录