Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 98161

Programs with Recursively Defined Data Structures

( Apr 20 – Apr 24, 1998 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:

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


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.

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