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
Creative work has been at the core of research in Human-Computer Interaction (HCI). I describe the results of a series of studies that look at how creators work, where creators include artists with years of professional practice, as well as learners, or novices and casual makers. My research focuses on three creation activities: drawing, physical modeling, and music composition. For these activities, I examine how artists switch between representations and how these representations evolve throughout their creative process, from early sketches to fine-grained forms or structured vocabularies. I present interactive systems that enrich their workflow (i) by extending their computer tools with physical user interfaces, or (ii) by making physical materials interactive. I also argue that sketch-based representations can allow for user interfaces that are more personal and less rigid. My presentation will reflect on lessons and limitations of this work and discuss challenges for future design-support tools.

Interactive visualizations combine human computer interaction, visual design, perception theory, as well as data processing methods in order to propose visual data representations that amplify cognition, and aid data exploration and understanding. We can consider visualization as a communication medium or channel between humans and their data. The higher the communication bandwidth (the data that can be communicated and understood), the more effective the visualization is. My research attempts to increase the bandwidth of this communication channel in the following two ways. (i) First, by moving away from traditional desktops towards larger displays that can both render larger amounts of data and can accommodate multiple viewers. (ii) And second, by designing and studying appropriate visual representations that show salient information. In my presentation I will describe my work on these topics, the challenges it tries to address, and discuss the methodology and inspiration behind this research.