This research is developing formal frameworks and methodologies for the verification and development of reactive systems: systems that maintain an ongoing interaction with their environment. The research concentrates on two tasks: modular verification, so that the correctness of an entire system can be derived from the correctness of its smaller components, and refinement, so that a high-level functional specification can be refined repeatedly, where each refinement step is formally proven to be a correct implementation of the former one. The techniques are being integrated into the STeP (Stanford Temporal Prover) system. ***
