# Verifying Relational Properties using Trace Logic

## TL;DR

This paper introduces a logical framework using trace logic for verifying relational properties in imperative programs, especially useful for security applications involving complex quantifier structures.

## Contribution

It develops a method to reduce relational property verification to first-order validity problems via trace logic, enabling reasoning about program traces and intermediate steps.

## Key findings

- Framework effectively verifies security-related relational properties.
- Trace logic supports reasoning about loop iterations and intermediate states.
- Implementation in Rapid demonstrates practical applicability.

## Abstract

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.