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

Inférence d'invariants pour le model checking de systèmes paramétrés

Starts on 03/10/2011
Advisor : CONCHON, Sylvain
[ZAIDI Fatiha]

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

Defended on 29/09/2014, committee :
Directeur de thèse :
- M. Sylvain Conchon, Professeur, Université Paris-Sud

Co-encadrante :
- Mme Fatiha Zaïdi, Maître de conférences, Université Paris-Sud

Rapporteurs :
- M. Ahmed Bouajjani, Professeur, Université Paris Diderot et IUF
- M. Silvio Ranise, Chercheur, Fondazione Bruno Kessler

Examinateurs :
- M. Rémi Delmas, Ingénieur de recherche, ONERA
- M. Alan Schmitt, Chargé de recherche, INRIA Rennes Bretagne Atlantique
- M. Philippe Dague, Professeur, Université Paris-Sud

Research activities :
   - Automated Proof, SMT and Applications

Abstract :
This thesis tackles the problem of automatically verifying complex
parameterized systems. This approach is important because it can guarantee that
some properties hold without knowing a priori the number of components in the
system. We focus in particular on the safety of such systems and we handle the
parameterized aspect with symbolic methods. This work is set in the theoretical
framework of the model checking modulo theories and resulted in a new model
checker: Cubicle.

One of the main contribution of this thesis is a novel technique for
automatically inferring invariants. The process of invariant generation is
integrated with the model checking algorithm and allows the verification in
practice of systems which are out of reach for traditional symbolic
approaches. One successful application of this algorithm is the safety analysis
of industrial size parameterized cache coherence protocols.

Finally, to address the problem of trusting the answer given by the model
checker, we present two techniques for certifying our tool Cubicle based on the
framework Why3. The first consists in producing certificates whose validity can
be assessed independently while the second is an approach by deductive
verification of the heart of Cubicle.

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.