April 20 – 24 , 1998, Dagstuhl Seminar 98161

Programs with Recursively Defined Data Structures


M. Schwartzbach (Aarhus), M. Sagiv (Tel Aviv), K. Weihe (Konstanz)

For support, please contact

Dagstuhl Service Team


Dagstuhl-Seminar-Report 207


To understand the difficulties in developing and implementing efficient data structures. This includes specification, verification, testing, and implementation.

More specifically, the goal is to bring together researchers from the following areas:

  1. Implementation of sophisticated data structures, e.g., libraries.
  2. Verification of partial correctness of such implementations, e.g., proving that a program only refers to allocated memory cells. In this group, one may also include program semantics.
  3. Efficient implementation of such programs, e.g., using sophisticated compile- time and run-time techniques. This includes running on advanced machines which includes intra- and inter-processor parallelism and improving other features, e.g. memory subsystem performance.

Currently, research in these related areas is mainly done in isolation. We feel that each of these groups can benefit quite a bit from understanding the potentials and the limitations of the research conducted by other groups.

For instance, very often an asymptotically fast algorithm will run slow in some (or even all) implementations. For example, locality of references can have big impact on memory subsystem performance through virtual memory and caching. Indeed, data structure researchers are consumers of the research produced by the imple mentors. Therefore, cooperation between these groups can be beneficial to both sides.

Research in verification may be consumed by both the data structure designers and the implementors. For example, testing the correctness of a data structure library routine can be quite a difficult task. Furthermore, it may be even difficult to show that the program does not dereference nil pointers.


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).

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.


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