# Relational properties for specification and verification of C programs in Frama-C

#### PhD Thesis

Author(s):Lionel Blatter
School:Université Paris-Saclay
Number:2019SACLC065
Year:2019
PDF:
URL:https://tel.archives-ouvertes.fr/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 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.

## BibTeX

@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.}
}