Many important properties of computer systems are relational properties, which are often difficult to express and verify. Dynamic logics are well-known formalisms for program verification. We present a general extension, called the rel extension, of dynamic logics to support first-class relational reasoning. The extension provides intuitive syntax to express relational properties, which may be difficult or impossible to express in the host dynamic logic. The rel extension can be instantiated for different host logics. Verifying relational properties expressed by the rel extension can benefit from techniques developed for general relational reasoning and domain-specific relational reasoning, and existing tools developed for the host logic.

We validate the applicability of the rel extension by instantiating it for a well-known dynamic logic: differential dynamic logic (dL). As a result, the instantiation can express key relational properties that cannot be easily expressed with dL. We develop an encoding for the instantiation to leverage existing verification tools for dL. We conduct an experiment on a set of benchmarks, and successfully verify a set of non-trivial relational properties either fully or semi automatically.