The deductive approach to verifying temporal properties of reactive systems is based on verification rules, which reduce the system validity of a temporal property to the general validity of first-order verification conditions. This methodology is complete relative to the underlying first-order reasoning. However, the proofs can be difficult to construct and understand, particularly as the complexity of the system increases.We have developed diagram-based formalisms for the verification of general temporal properties of reactive, real-time and hybrid systems. A diagram is a visual abstraction of the system to be verified; it represents the aspects of the system relevant to the property to be proved. The diagram represents a schematic overview of a deductive proof, and therefore it is more intuitive and easier to construct and understand.These methods combine deductive and algorithmic verification, and are being extended to include modularity, abstraction and refinement to facilitate the verification of larger, more complex systems.