Deductive verification techniques provide powerful methods for formal verification of
properties expressed in Hoare Logic. In this formalization, also
known as axiomatic semantics, a program is seen as a predicate transformer, where each
program *c* executed on a state verifying a property P leads to a state verifying
another property *Q*.

Relational properties, on the other hand, link *n* programs to two properties.
More precisely, a relational property is a property about *n* programs
*c₁*, ..., *cₙ* stating that if each program *cᵢ* starts in a state
*sᵢ* and ends in a state *s0ᵢ* such that *P(s₁, ..., sₙ)* holds, then
*Q(s0₁, ..., s0ₙ)* holds. Thus, relational properties invoke any finite number of
executions of possibly dissimilar programs.

Such properties cannot be expressed directly in the traditional setting of modular
deductive verification, as axiomatic semantics cannot refer to two distinct executions
of a program *c*, or different programs *c₁* and *c₂*.

This thesis brings two solutions to the deductive verification of relationalproperties.
Both of them make it possible to prove a relational property and to use it as a hypothesis
in the subsequent verifications. We model our solutions using a small imperative language
containing procedure calls.

Both solutions are implemented in the context of the C programming language, the
FRAMA-C platform, the ACSL specification language and the deductive verification
plugin WP. The new tool, called RPP, allows one to specify a relational property,
to prove it using classic deductive verification, and to use it as hypothesis in the
proof of other properties. The tool is evaluated over a set of illustrative examples.

Experiments have also been made on runtime checking of relational properties and
counterexample generation when a property cannot be proved.

@phdthesis{blatter19,
title = {Relational properties for specification and verification
of {C} programs in {Frama-C}},
author = {Lionel Blatter},
url = {https://tel.archives-ouvertes.fr/tel-02401884},
number = {2019SACLC065},
school = {{Universit{\'e} Paris-Saclay}},
year = {2019},
month = sep,
pdf = {https://tel.archives-ouvertes.fr/tel-02401884/file/74175_BLATTER_2019_diffusion.pdf},
hal_id = {tel-02401884},
abstract = {Deductive verification techniques provide powerful methods for formal verification of
properties expressed in Hoare Logic. In this formalization, also
known as axiomatic semantics, a program is seen as a predicate transformer, where each
program \emph{c} executed on a state verifying a property P leads to a state verifying
another property \emph{Q}.
\newline
Relational properties, on the other hand, link \emph{n} programs to two properties.
More precisely, a relational property is a property about \emph{n} programs
\emph{c₁}, ..., \emph{cₙ} stating that if each program \emph{cᵢ} starts in a state
\emph{sᵢ} and ends in a state \emph{s0ᵢ} such that \emph{P(s₁, ..., sₙ)} holds, then
\emph{Q(s0₁, ..., s0ₙ)} holds. Thus, relational properties invoke any finite number of
executions of possibly dissimilar programs.
\newline
Such properties cannot be expressed directly in the traditional setting of modular
deductive verification, as axiomatic semantics cannot refer to two distinct executions
of a program \emph{c}, or different programs \emph{c₁} and \emph{c₂}.
\newline
This thesis brings two solutions to the deductive verification of relationalproperties.
Both of them make it possible to prove a relational property and to use it as a hypothesis
in the subsequent verifications. We model our solutions using a small imperative language
containing procedure calls.
\newline
Both solutions are implemented in the context of the C programming language, the
{FRAMA-C} platform, the {ACSL} specification language and the deductive verification
plugin {WP}. The new tool, called {RPP}, allows one to specify a relational property,
to prove it using classic deductive verification, and to use it as hypothesis in the
proof of other properties. The tool is evaluated over a set of illustrative examples.
\newline
Experiments have also been made on runtime checking of relational properties and
counterexample generation when a property cannot be proved.}
}