Checking linked data structures Conference Paper uri icon

abstract

  • In the program checking paradigm, the original program is run on the desired input, and its output is checked by another program called a checker. Recently, the notion of program checking has been extended from its original formulation of checking functions to checking a sequence of operations which query and alter the state of an object external to the program, e.g., checking the interactions between a client and the manager (server) of a data structure. In this expanded paradigm, the checker acts as an intermediary between the client, which generates the requests, and the server, which processes them. The checker is allowed a small amount of reliable memory and may provide a probabilistic guarantee of correctness for the client. We present off-line and on-line checkers for data structures such as linked lists, trees, and graphs. Previously, the only data structures for which such checkers existed were random access memories, stacks, and queues.

published proceedings

  • Digest of Papers - International Symposium on Fault-Tolerant Computing

author list (cited authors)

  • Amato, N. M., & Loui, M. C.

complete list of authors

  • Amato, NM||Loui, MC

publication date

  • January 1994

published in