Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Dissertations & habilitations
Research results
Ph.D de

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.

Ph.D. dissertations & Faculty habilitations


The topic of this habilitation is the study of very small data visualizations, micro visualizations, in display contexts that can only dedicate minimal rendering space for data representations. For several years, together with my collaborators, I have been studying human perception, interaction, and analysis with micro visualizations in multiple contexts. In this document I bring together three of my research streams related to micro visualizations: data glyphs, where my joint research focused on studying the perception of small-multiple micro visualizations, word-scale visualizations, where my joint research focused on small visualizations embedded in text-documents, and small mobile data visualizations for smartwatches or fitness trackers. I consider these types of small visualizations together under the umbrella term ``micro visualizations.'' Micro visualizations are useful in multiple visualization contexts and I have been working towards a better understanding of the complexities involved in designing and using micro visualizations. Here, I define the term micro visualization, summarize my own and other past research and design guidelines and outline several design spaces for different types of micro visualizations based on some of the work I was involved in since my PhD.