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
APPRENTISSAGE ET OPTIMISATION SUR LES GRAPHES


ANALYSE DE DONNéES MULTI-MODALES POUR LES PATHOLOGIES COMPLEXES PAR LA CONCEPTION ET L’IMPLéMENTATION DE PROTOCOLES REPRODUCTIBLES ET RéUTILISABLES


DESIGNING INTERACTIVE TOOLS FOR CREATORS AND CREATIVE WORK
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.