How to leave out details: error-preserving abstractions of state-space models

Analyses based on state-space models of execution must omit some details of execution, in order to fold the infinite space of possible program executions into a sufficiently small space for analysis. These simplifications are generally justified by a claim that the resulting analysis is conservative with respect to a certain class of faults, i.e. that the simplification will not cause any faults to be overlooked in the analysis. The author formalized a notion of error-preserving abstractions which captures this claim, gives sufficient conditions for verifying this property in practical cases, and discusses the role of error-preserving abstractions in combining fault detection techniques