Typing, Analysis and Verification of Heap-Manipulating Programs

Summary

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 central purpose of this Dagstuhl seminar was to bring together top researchers from these three different communities and to investigate the synergies that can result from a combination of the techniques developed by these communities.

Participants and Organization

The seminar had 41 participants with a good distribution over the three research communities mentioned above. We were in particularly happy to have a good number of excellent young researchers as participants.

After the Monday morning sessions where each participant gave a short statement of his/her background and interest, we started with four overview talks covering the central topics and views of the different communities:

• Peter Müller: Ownership based types
• K. Rustan M. Leino: Comparing heap models: Ownership, dynamic frames, permissions
• Greta Yorsh: Shape analysis overview
• Viktor Kuncak: Theorem provers and decision procedures

The rest of the seminar was structured into research presentations (31 talks), presentation of challenge problems (three problems were presented and discussed), and discussions on how to exploit potential synergies of the different techniques.

Remarks on synergies

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. A good witness of the close relation between functional and structural properties is separation logic.