Typing, Analysis and Verification of Heap-Manipulating Programs

Motivation

Most of today's software is written in procedural or object-oriented programming languages. Many of these programs make use of heap-allocated data. This is in particular true for object-oriented programs. Thus, analysis and verification techniques for heap-manipulating programs are crucial to avoid and find errors, to optimize implementations, and to verify properties in a huge class of modern software.

The heap has been a major obstacle to more widespread use of verification and analysis for real-world code. In the last ten years, though, research on analysis and verification for heap-manipulating programs has progressed significantly, in work mainly done by three research communities:

1. Ownership and region types for structuring object heaps, for alias control, and for encapsulation. The main idea is to restrict the way pointers are manipulated and/or restrict the shape of the heap.
2. Verification of heap manipulating programs. The main idea is to specify interesting properties of such programs and to develop formal methods for checking if the specifications are met by the program.
3. Static program analysis for heaps. The main idea is to automatically infer properties of programs. For example, many algorithms infer the shape of the heap at various program points.

The purpose of this Dagstuhl seminar is to bring together top researchers from these three different communities.

The three areas complement each other and can provide many synergies. We expect benefits to all communities. For example, ownership type information can be useful to static analyses and deductive verification. Analysis techniques can support type inference, allow generalizing type systems, and can automatically provide information for verification frameworks. Heap structuring techniques used in verification frameworks, like in separation logic, can be helpful to modularize static analyses. Besides combination of the techniques, another dimension of integration is given by the properties of interest such as, e.g., alias control, access modes, encapsulation, heap structure properties, and behavioral interface properties.

Often these properties have to be analyzed together. E.g., certain heap analyses can only be applied in a modular way if the program satisfies some encapsulation restrictions. Also, programs that satisfy ownership requirements may be amenable to more efficient program analysis. That separation logic makes structural reasoning explicit in the logic is a good witness of the close relation between functional and structural properties.

Research Questions

The following research questions give a first impression on the possible interactions and synergies between these groups:

1. What are the right semantic notions of ownership and encapsulation?
2. What is the right notion of ownership which permits flexible enough programming styles and can be effectively checked?
3. What is the granularity of the program in which ownership need to be enforced? Are class invariants obsolete?
4. How can ownership techniques improve the modularity of static analyses?
5. How can abstract-interpretation-based static analyses be integrated into deductive verification, e. g. using separation logic?
6. What insight can be gained from the frame rule for static analysis?
7. How can static analysis in this area be used for inference of ownership types?

Proposed General Organization

The first three days will consist of talks from each of the communities followed by a discussion on how the presented techniques can be used or improved by the approaches of the other two communities. Thursday and Friday are devoted to topics crossing the communities. The goal is to develop a report on the remaining open questions in the intersection of the three areas. The report will also sketch a road map that concerns how the techniques should be integrated into future languages and programming systems.