Authors: Nancy M. Amato and Michael C. Loui

Venue: Proceedings of IEEE 24th International Symposium on Fault-Tolerant Computing
DOI: 10.1109/FTCS.1994.315644
Link to Publication

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. 

@inproceedings{Loui-clds-1994, 
 author = {Nancy M. Amato and Michael C. Loui}, 
 booktitle = {Proceedings of the 24th Annual International Symposium on Fault-Tolerant Computing (FTCS)}, 
 doi = {10.1109/FTCS.1994.315644}, 
 pages = {164--173}, 
 title = {Checking Linked Data Structures}, 
 year = {1994} 
}