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-Sud
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 original manuscript conceptualizes the recent rise of digital platforms along three main dimensions: their nature of coordination devices fueled by data, the ensuing transformations of labor, and the accompanying promises of societal innovation. The overall ambition is to unpack the coordination role of the platform and where it stands in the horizon of the classical firm – market duality. It is also to precisely understand how it uses data to do so, where it drives labor, and how it accommodates socially innovative projects. I extend this analysis to show continuity between today’s society dominated by platforms and the “organizational society”, claiming that platforms are organized structures that distribute resources, produce asymmetries of wealth and power, and push social innovation to the periphery of the system. I discuss the policy implications of these tendencies and propose avenues for follow-up research.