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

Ph.D
Group : Verification of Algorithms, Languages and Systems

Tools and Techniques for the Verification of Modular Stateful Code

Starts on 01/05/2015
Advisor : FILLIÂTRE, Jean-Christophe

Funding : Bourse pour étudiant étranger
Affiliation : Université Paris-Sud
Laboratory : LRI - VALS

Defended on 10/12/2018, committee :
Directeur de thèse:
- M. Jean-Christophe FILLIATRE, CNRS

Rapporteurs :
- M. Jorge SOUSA PINTO, Universidade do Minho
- M. Wolfgang AHRENDT, Chalmers University of Technology

Examinateurs :
- Mme Catherine DUBOIS, Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise
- Mme Mihaela SIGHIREANU, Université Paris Diderot
- M. Xavier LEROY, INRIA
- M. Laurent FRIBOURG, CNRS

Research activities :

Abstract :
This thesis is set in the field of formal methods, more precisely in the domain of deductive program verification. Our working context is the Why3 framework, a set of tools to implement, formally specify, and prove programs using off-the-shelf theorem provers. Why3 features a programming language, called WhyML, designed with verification in mind. An important feature of WhyML is ghost code: portions of the program that are introduced for the sole purpose of specification and verification. When it comes to get an executable implementation, ghost code is removed by an automatic process called extraction. One of the main contributions of this thesis is the formalization and implementation of Why3's extraction. The formalization consists in showing that the extracted program preserves the same operational behavior as the original source code, based on a type and effect system. The new extraction mechanism has been successfully used to get correct-by-construction OCaml modules, which are part of a verified OCaml library of data structures and algorithms. This verification effort led to two other contributions of this thesis. The first is a systematic approach to the verification of pointer-based data structures using ghost models of fragments of the heap. A fully automatic verification of a union-find data structure was achieved using this technique. The second contribution is a modular way to reason about iteration, independently of the underlying implementation. Several cursors and higher-order iterators have been specified and verified with this approach.

Ph.D. dissertations & Faculty habilitations
DECODING THE PLATFORM SOCIETY: ORGANIZATIONS, MARKETS AND NETWORKS IN THE DIGITAL ECONOMY
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.

DISTRIBUTED COMPUTING WITH LIMITED RESOURCES


VALORISATION DES DONNéES POUR LA RECHERCHE D'EMPLO