Ph.D
Group : Verification of Algorithms, Languages and Systems
Un système de types pragmatique pour la vérification déductive des programmes
Starts on 01/10/2013
Advisor : FILLIÂTRE, Jean-Christophe
Funding : contrat doctoral UPS
Affiliation : Université Paris-Saclay
Laboratory : LRI VALS
Defended on 13/12/2016, committee :
Directeurs de thèse :
- M. Jean-Christophe Filliâtre, CNRS, Université Paris Sud
- M. Andrei Paskevich, Université Paris Saclay
Rapporteurs :
- Mme Sandrine Blazy, Université de Rennes 1
- M. Jorge Sousa Pinto, Universidade de Minho
Examinateurs :
- M. Giuseppe Castagna, CNRS, Université de Paris 7
- M. Jean Goubault-Larrecq, LSV, CNRS, ENS Cachan
- M. François Pottier, INRIA Paris
Research activities :
- Deductive Verification of Programs
Abstract :
This thesis is conducted in the framework of deductive software verification.
is aims to formalize some concepts that are implemented in the verification
tool Why3. The main idea is to explore solutions that a type system based
approach can bring to deductive verification.
First, we focus our attention on the notion of ghost code, a technique
that is used in most of modern verification tools and which consists in giving
to some parts of specification the appearance of operational code.
Using ghost code correctly requires various precautions since the ghost code
must never interfere with the operational code. The first contribution of my
thesis consists in a formal study of the ghost code in which I show how a type
system with effects allows ghost code to be used in a way which is both correct
and expressive.
The second contribution of my thesis in related to verification of programs
with pointers in the presence of aliasing, i.e. when several pointers handled
by a program denote a same memory cell. Rather than moving towards to
approaches that address the problem in all its complexity to the costs of
abandoning the framework of Hoare logic, we present a type system with effects
and singleton regions which resolves aliasing issues by performing a static
control of aliases even before the proof obligations are generated. Although
our system is limited to pointers whose identity must be known statically, we
observe that it fits for most of the code we want to verify.
Finally, we focus our attention on a situation where there exists an
abstraction barrier between the user's code and the one of the libraries which
it depends on. That means that libraries provide the user a set of functions
and of data structures, without revealing details of their implementation. When
programs are developed in a such modular way, verification must be modular
itself. It means that the verification of user's code must take into account
only function contracts supplied by libraries while the verification of
libraries must ensure that their implementations refine correctly the exposed
entities. The third contribution of my work is to extend the system presented
in the previous with these concepts of modularity and data refinement, showing
that static control of aliases is an ingredient both necessary and original for
the data refinement in Why3.
_________________________________
