Verifying temporal specifications of reactive and concurrent systems commonly relies on generating auxiliary assertions and strengthening given properties of the system. Two dual approaches find solutions to these problems: the bottom-up method performs an abstract forward propagation of the system, generating auxiliary properties; the top-down method performs an abstract backward propagation to strengthen given properties. Exact application of these methods is complete but is usually infeasible for large-scale verification. An approximate analysis can often supply enough information to complete the verification.
The paper overviews some of the exact and approximate analysis methods to generate and strengthen assertions for the verification of invariance properties. By formulating and analyzing a generic safety verification rule we extend these methods to the verification of general temporal safety properties.