  Reactive programs are ubiquitous in modern applications, and so verification
is highly desirable. We present a verification strategy for reactive programs
with a large or infinite state space utilising algebraic laws for reactive
relations. We define novel operators to characterise interactions and state
updates, and an associated equational theory. With this we can calculate a
reactive program's denotational semantics, and thereby facilitate automated
proof. Of note is our reasoning support for iterative programs with reactive
invariants, which is supported by Kleene algebra. We illustrate our strategy by
verifying a reactive buffer. Our laws and strategy are mechanised in
Isabelle/UTP, which provides soundness guarantees, and practical verification
support.
