Verifying Relational Properties using Trace Logic

Gilles Barthe, Renate Eilers, Pamina Georgiou +3

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 applica…