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
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