Adaptive Heap Analysis

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

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.