Adaptive Heap Analysis

软件是现代生活的一个关键元素。它无处不在，控制着我们社会所依赖的许多基本服务和系统。因此，高质量的软件是绝对重要的。然而，不幸的是，软件几乎总是包含错误——被称为bug——因此行为不端。这些错误是由于代码的大小和复杂性造成的：现代代码是如此庞大和复杂，以至于今天的技术无法检测到其中的许多错误。现实代码中复杂性的主要来源之一是大量使用动态分配内存（称为堆）来存储重要的数据结构。但是，在使用堆时出现的编程错误很难避免，甚至很难检测到。堆分析（通常称为形状分析）是一种程序分析，旨在为使用堆的程序提供准确的结果。由于需要对指针进行推理，堆分析是最难的程序分析之一，并且被认为是一个主要的开放问题。许多程序分析（例如那些寻址数值属性的程序）都是全自动和通用的，因此为大多数程序提供了有意义的结果。不幸的是，在堆分析的情况下并非如此。目前，它们中的大多数都是临时的，只适用于大量特定的（硬连接的）数据结构。如果一个程序碰巧没有使用这些结构中的一个，就会得到不精确（无用）的结果。这是一个问题，因为实际软件中使用的数据结构的多样性很大。这使得堆分析在实际应用中变得非自动化，从一个程序到另一个程序需要设计新的定制技术。反过来，这使得它的应用成本令人望而却步。因此，较差的通用性和自动化是阻碍堆分析在实际程序验证中的应用的主要因素。该项目旨在解决这些问题，这些问题是使堆分析适用于学术界以外的关键途径。提出了一种方法，使分析能够适应被分析程序的数据结构。自适应可以提供必要的灵活性和通用性，使堆分析自动化。这个项目的成功将为自动分析技术的应用提供重要的步骤，以验证实质性的、真实的代码。

Software is a key element of modern life. It is pervasive and controls manyfundamental services and systems our society depends upon. Therefore high qualitysoftware is absolutely vital. Unfortunately, however, software nearly alwayscontains mistakes - called bugs - and therefore misbehaves. These bugs are due to the size and complexity of the code: modern code is so large and complicatedthat today's technology cannot detect many of them.One of the major source of complexity in real-life code is the intensive use of dynamic allocated memory (called the heap) for storing important data structures.But programming error in the use of the heap is notoriously difficult to avoid and even detect.Heap analyses (often called shape analyses) are program analyses meant to give accurate resultsfor programs using the heap. Having to reason about pointers,heap analysis is one of the hardest kinds of program analysis, and is considered a major open problem.Many program analyses (e.g. those addressing numerical properties) areboth fully automatic and general, therefore providing meaningfulresults for most programs. This is unfortunately not true in the caseof heap analysis. Currently, most of them are ad-hoc and work only for ahand-full of specific (hard-wired) data structures.If a program happens not to use one of these structures imprecise (useless) results will be delivered. This is a problem because the variety of data structures used in real software is great.It makes heap analysis in practice non-automatic: from program to program new tailored techniquesneed to be designed. In turn, this makes its cost of application prohibitive. Thus, poor generality and automation are major factorshindering the application of heap analysis to verification of real programs.This project aims to address these issues, which are on the criticalpath to making heap analysis applicable outside academia. It proposesto develop methodologies to make an analysis adapt on-the-flyto the data structures of the analysed program. Adaptation can providethe necessary flexibility and generality to make heap analysis automatic.Success in this project will provide significant steps towards theapplication of automatic analysis techniques to verification of substantial, real-world code.