  Deductive verification typically relies on function contracts that specify
the behavior of each function for a single function call. Relational properties
link several function calls together within a single specification. They can
express more advanced properties of a given function, such as non-interference,
continuity, or monotonicity, or relate calls to different functions, possibly
run in parallel, for instance, to show the equivalence of two implementations.
However, relational properties cannot be expressed and verified directly in the
traditional setting of modular deductive verification. Recent work proposed a
new technique for relational property verification that relies on a
verification condition generator to produce logical formulas that must be
verified to ensure a given relational property. This paper presents an overview
of this approach and proposes important enhancements. We integrate an optimized
verification condition generator and extend the underlying theory to show how
relational properties can be proved in a modular way, where one relational
property can be used to prove another one, like in modular verification of
function contracts. Our results have been fully formalized and proved sound in
the Coq proof assistant.
