  We present a logical framework for the verification of relational properties
in imperative programs. Our work is motivated by relational properties which
come from security applications and often require reasoning about formulas with
quantifier-alternations. Our framework reduces verification of relational
properties of imperative programs to a validity problem into trace logic, an
expressive instance of first-order predicate logic. Trace logic draws its
expressiveness from its syntax, which allows expressing properties over
computation traces. Its axiomatization supports fine-grained reasoning about
intermediate steps in program execution, notably loop iterations. We present an
algorithm to encode the semantics of programs as well as their relational
properties in trace logic, and then show how first-order theorem proving can be
used to reason about the resulting trace logic formulas. Our work is
implemented in the tool Rapid and evaluated with examples coming from the
security field.
