Recently, a novel approach for runtime verification of complex superscalar processors has been proposed. In this approach, every computation is dynamically verified by hardware using a form of complete induction. This project focuses on extending the notion of inductive dynamic verification to the general case of parallel distributed systems. The principles of dynamic inductive checking for parallel semantics are investigated. This includes an understanding of the characteristics and properties of systems, where the approach can be used effectively. The initial vehicles used for developing such techniques are the problems of cache coherence and support for sequential consistency in shared-memory multiprocessors. As a natural extension of this research, the project formulates a method for state machine abstraction, which can be applied in the general case. This method rests on the separation of architected state from additional implementation state, and the identification of that subset of state transitions that correspond to changes in the architected state only.
