http://www.dagstuhl.de/09301

July 19 – 24 , 2009, Dagstuhl Seminar 09301

Typing, Analysis and Verification of Heap-Manipulating Programs

Organizers

Peter O'Hearn (Queen Mary University of London, GB)
Arnd Poetzsch-Heffter (TU Kaiserslautern, DE)
Mooly Sagiv (Tel Aviv University, IL)



The Dagstuhl Foundation gratefully acknowledges the donation from:

  •   Microsoft Research, Cambridge, UK

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Seminar Proceedings DROPS
List of Participants
Dagstuhl Seminar Schedule [pdf]

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 di erent 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 di fferent 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 di erent techniques.

Remarks on synergies

Ownership type information can be useful to static analyses and deductive verifi cation. Analysis techniques can support type inference, allow generalizing type systems, and can automatically provide information for veri cation frameworks. Heap structuring techniques used in verifi cation 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 satisfi es 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.

Classification

  • Programming Languages
  • Compiler
  • Semantics
  • Specification
  • Formal Methods
  • Verification
  • Logic

Keywords

  • Separation Logic
  • Shape Analysis

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, 1st floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.