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

Ph.D
Group : Toccata

Verification of Programs With Pointers Using Regions and Permissions

Starts on 01/09/2007
Advisor : MARCHÉ, Claude

Funding : AM
Affiliation : Université Paris-Sud
Laboratory : LRI PROVAL

Defended on 14/10/2011, committee :
Peter Müller
François Pottier
Jean Goubault-Larrecq
Burkhart Wol
Claude Marché

Research activities :

Abstract :
Deductive verification consists in annotating programs by a
specification, i.e. logic formulas which describe the behavior of the
program, and prove that programs verify their specification. Tools such
as the Why platform take a program and its specification as input and
compute logic formulas such that, if they are valid, the program
verifies its specification. These logic formulas can be proven
automatically or using proof assistants.

When a program is written in a language supporting pointer aliasing,
i.e. if several variables may denote the same memory cell, then
reasoning about the program becomes particularly tricky. It is necessary
to specify which pointers may or may not be equal. Invariants of data
structures, in particular, are harder to maintain.

This thesis proposes a type system which allows to structure the heap in
a modular fashion in order to control pointer aliases and data
invariants. It is based on the notions of region and permission.
Programs are then translated to Why such that pointers are separated as
best as possible, to facilitate reasoning. This thesis also proposes an
inference mechanism to alleviate the need to write region operations
introduced by the language. A model is introduced to describe the
semantics of the language and prove its safety. In particular, it is
proven that if the type of a pointer tells that its invariant holds,
then this invariant indeed holds in the model. This work has been
implemented as a tool named Capucine. Several examples have been written
to illustrate the language, and where verified using Capucine.

More information: http://romain.bardou.fr/misc/sujetthese.pdf
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