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.