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

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