Hoare-style program logics are a popular and
effective technique for software
verification. Relational program logics are an
instance of this approach that enable reasoning
about relationships between the execution of two
or more programs. Existing relational program
logics have focused on verifying
that all runs of a collection of
programs do not violate a specified relational
behavior. Several important relational
properties, including refinement and
noninterference, do not fit into this category,
as they also mandate the existence
of specific desirable executions. This paper
presents RHLE, a logic for verifying these sorts
of relational ∀∃-properties. Key to
our approach is a novel form of function
specification that employs a variant of ghost
variables to ensure that valid implementations
exhibit certain behaviors. We have used a
program verifier based on RHLE to verify a
diverse set of relational
∀∃-properties drawn from the
literature.
