Dagstuhl Seminar 98161
Programs with Recursively Defined Data Structures
( Apr 20 – Apr 24, 1998 )
Permalink
Organizers
- K. Weihe (Konstanz)
- M. Sagiv (Tel Aviv)
- M. Schwartzbach (Aarhus)
Contact
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:
- Implementation of sophisticated data structures, e.g., libraries.
- 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.
- 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)