Dagstuhl Seminar 09301
Typing, Analysis and Verification of Heap-Manipulating Programs
( Jul 19 – Jul 24, 2009 )
- Peter O'Hearn (Queen Mary University of London, GB)
- Arnd Poetzsch-Heffter (TU Kaiserslautern, DE)
- Mooly Sagiv (Tel Aviv University, IL)
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:
- 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.
- 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.
- 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.
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.
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.
- Jonathan Aldrich (Carnegie Mellon University, US) [dblp]
- Daphna Amit (Tel Aviv University, IL)
- Andrew W. Appel (Princeton University, US) [dblp]
- Anindya Banerjee (IMDEA Software - Madrid, ES) [dblp]
- Michael Barnett (Microsoft Corporation - Redmond, US)
- Nick Benton (Microsoft Research UK - Cambridge, GB) [dblp]
- Joshua Berdine (Microsoft Research UK - Cambridge, GB) [dblp]
- Richard Bornat (Middlesex University, GB) [dblp]
- Ahmed Bouajjani (University of Paris VII, FR) [dblp]
- Cristiano Calgano (Imperial College London, GB)
- Bor-Yuh Evan Chang (University of Colorado - Boulder, US) [dblp]
- Dave Clarke (KU Leuven, BE) [dblp]
- David Cok (Eastman Kodak Comp. - Rochester, US) [dblp]
- Dino Distefano (Queen Mary University of London, GB) [dblp]
- Sophia Drossopoulou (Imperial College London, GB) [dblp]
- Philippa Gardner (Imperial College London, GB) [dblp]
- Alexey Gotsman (University of Cambridge, GB) [dblp]
- Peter Habermehl (University of Paris VII, FR) [dblp]
- Martin Hofmann (LMU München, DE) [dblp]
- Jörg Kreiker (TU München, DE)
- Viktor Kuncak (EPFL - Lausanne, CH) [dblp]
- Gary T. Leavens (University of Central Florida - Orlando, US) [dblp]
- K. Rustan M. Leino (Microsoft Corporation - Redmond, US) [dblp]
- Etienne Lozes (ENS - Cachan, FR)
- Roman Manevich (UCLA, US) [dblp]
- Peter Müller (ETH Zürich, CH) [dblp]
- David A. Naumann (Stevens Institute of Technology, US) [dblp]
- James Noble (Victoria University - Wellington, NZ) [dblp]
- Peter O'Hearn (Queen Mary University of London, GB) [dblp]
- Arnd Poetzsch-Heffter (TU Kaiserslautern, DE) [dblp]
- Ganesan Ramalingam (Microsoft Research India - Bangalore, IN) [dblp]
- Noam Rinetzky (Queen Mary University of London, GB) [dblp]
- Xavier Rival (ENS - Paris, FR) [dblp]
- Mooly Sagiv (Tel Aviv University, IL) [dblp]
- Peter Sestoft (IT University of Copenhagen, DK) [dblp]
- Elodie-Jane Sims (ENS - Paris, FR)
- Tomas Vojnar (Brno University of Technology, CZ) [dblp]
- Thomas Wies (EPFL - Lausanne, CH) [dblp]
- Reinhard Wilhelm (Universität des Saarlandes, DE) [dblp]
- Hongseok Yang (Queen Mary University of London, GB) [dblp]
- Greta Yorsh (IBM TJ Watson Research Center - Yorktown Heights, US) [dblp]
- programming languages
- formal methods
- Separation Logic
- Shape Analysis