Dans un contexte économique complexe, l’implication des managers dans la formationde leurs collaborateurs parait importante. Au sein d’un groupe français automobile et d’unemultinationale en sécurité numérique, nous essayons d’identifier les différents rôles desmanagers dans la formation, les effets de ces rôles, les difficultés et enfin les conditionsrequises pour mener à bien ces rôles.Les managers vivent actuellement un malaise et il est certain que leur position lesconfronte à de multiples contraintes. Les activités de travail et de formation se confondent deplus en plus: les activités de travail viennent se placer au coeur de la formation et les activitésde formation investissent les lieux de travail: d’où l’intérêt d’étudier les rôles des managersdans la formation formelle et informelle.Pour répondre à notre objectif de recherche, nous avons eu recours à la méthode derecherche qualitative par des entretiens semi-directifs. Il en est ressorti que les managers sontfortement impliqués dans la formation : de l’animation des sessions de formation, jusqu’ausuivi et transfert des connaissances au quotidien.Notre recherche met l’accent sur les rôles « formateur » du manager dans un contexted’instabilité; en effet, l’implication volontaire des managers à former eux-mêmes leurscollaborateurs peut s’expliquer en grande partie par la complexité du contexte qui exige de lapart des managers d’agir en urgence afin de dépasser les défaillances dues à la lourdeur et à lalenteur des processus de formation formelle. / In a complex economic environment, the involvement of managers in training theiremployees seems important. In a French automotive group and a multinational in digitalsecurity, we try to identify the different roles of managers in training, the effects of theseroles, challenges and finally the requirements to carry out these roles.Now, managers live discomfort and it is certain that their position confronts them tomultiple constraints. Work and training activities merge more and more: work activities areplaced at the heart of education and training activities are investing in the workplace: hencethe need to study managers’ roles in the formal and informal training.To answer our research goal, we used the qualitative research method by semistructuredinterviews. It found that managers are heavily involved in training: from animatingtraining sessions until monitoring and knowledge transfer in day to day activities.Our research highlights the “trainer” roles of the manager in a context of instability.Indeed, the personal involvement of managers to train their team can be largely explained bythe complexity of the context that requires from them to act urgently to overcome failures dueto the complexity and the slowness of the formal training process.

Cette thèse appartient au domaine des méthodes formelles. Nous nous concentrons sur leur application à une méthodologie spécifique pour le développement de logiciels: l'ingénierie à base de composants. Le Grid Component Model (GCM) suit cette méthodologie en fournissant tous les moyens pour définir, composer, et dynamiquement reconfigurer les applications distribuées à base de composants. Dans cette thèse, nous abordons la spécification formelle, la vérification et le déploiement d'applications GCM reconfigurables et distribuées. Notre première contribution est un cas d'étude industriel sur la spécification comportementale et la vérification d'une application distribuée et reconfigurable: L'HyperManager. Notre deuxième contribution est une plate-forme, élaborée avec l'assistant de preuve Coq, pour le raisonnement sur les architectures logicielles: Mefresa. Cela comprend la mécanisation de la spécification du GCM, et les moyens pour raisonner sur les architectures reconfigurables GCM. En outre, nous adressons les aspects comportementaux en formalisant une sémantique basée sur les traces d'exécution de systèmes de transitions synchronisées. Enfin, notre troisième contribution est un nouveau langage de description d'architecture (ADL): Painless. En outre, nous discutons son intégration avec ProActive, un intergiciel Java pour la programmation concurrente et distribuée, et l'implantation de référence du GCM. / This thesis belongs to the domain of formal methods. We focus their application on a specific methodology for the development of software: component-based engineering.The Grid Component Model (GCM) endorses this approach by providing all the means to define, compose and dynamically reconfigure component-based distributed applications. In this thesis we address the formal specification, verification and deployment of distributed and reconfigurable GCM applications. Our first contribution is an industrial case study on the behavioural specification and verification of a reconfigurable distributed application: The HyperManager. Our second contribution is a framework, developed with the Coq proof assistant, for reasoning on software architectures: Mefresa. This encompasses the mechanization of the GCM specification, and the means to reason about reconfigurable GCM architectures. Further, we address behavioural concerns by formalizing a semantics based on execution traces of synchronized transition systems. Overall, it provides the first steps towards a complete specification and verification platform addressing both architectural and behavioural properties. Finally, our third contribution is a new Architecture Description Language (ADL), denominated Painless. Further, we discuss its proof-of-concept integration with ProActive, a Java middleware for concurrent and distributed programming, and the de facto reference implementation of the GCM.

In Sein und Zeit Heidegger décrit le caractère émotif de la structure ontologique de l’existence en tant que Befiindlichkeit. Le sentiment de la situation vient de l'expérience ontique du quotidien comme une Stimmung. Celle-ci en tant qu'indication formelle renvoit de expérience ontique vers la constitution ontologique du Dasein. Les deux sont pensés au début dans une relation simple d’accompagnement. Pourtant à partir de 1930 le terme Befindlichkeit disparaît, et à sa place nous trouverons la seule disposition émotive ontique. Ce travail commence par demander les raisons de cette disparition. Le motif le plus important c’est que Heidegger s’est aperçu de la nécessité de soumettre même les phénomènes émotifs dont il s’agit au renversement du tournant, la Kehre. Dans cette nouvelle démarche de la pensée c’est le caractère d’événement des dispositions émotives qui doit être dégager. Dans le processus visé à le saisir, on découvre le pouvoir des dispositions de modifier à la racine la pensée, permettant à celle-ci de se déployer autrement que la métaphysique. Il s’agit de dépasser la représentation en tant que modalité fondamentale de la pensée pour découvrir l’essence des images dans le langage poétique. cela se montre comme unique possibilité de garder l’être dans l’étant. / In Time and being Heidegger describes the emotional character of the ontological structure of existence as a Befindlichkeit. The state of mind occurs on the ontical experience of everyday as a Stimmung, which in its phenomenological function as formal indication defers to the ontological structure of Dasein. The relation between them seems to be that of simple accompaniment. Within the turn this relation undergoes a reversal, so that the term Befindlichkeit itself disappears to leave only the Stimmung. While in 1926 the onticity of Stimmung was considered inauthentic, within the Kehre, however, this ontical layer always emotionally disposed, reveals the access to the original in the Daseins facticity. The ontic-ontological structure unfolds the ambiguity of truths as duplicity of the emotional openness of Dasein, so that it would have definitely been perceived in the early 1930’s as ontical Stimmung. In this way Heidegger strengthens its function, so far as to make it indispensable for the preparation of the other beginning of thinking. If the representational thinking depends on the Grundstimmung of the first beginning, as well as on the fact that metaphysics do not question ask about the truth of being, but rather pursue the question of the entity until the calculating thought of the technological epoch, then the thought of the other beginning must not only forbid the representation, but also, at the same time, rediscover the disclosing essence of the image. Once poetry is understood as original language, poetry’s use of image offers the possibility to bring the appropriative event to the language without objectifying it. The ability to safeguard the being into a word that does not represent it but just states it, indicating its happening, depends on the correct understanding of the event’s character of Stimmungen.

Le développement des réseaux de communication digitaux tel Internet a rendu omniprésents les protocoles de communication. Les différents appareils électroniques que nous utilisons au quotidien doivent interagir les uns avec les autres afin de réaliser les taches nombreuses et variées qui sont devenues courantes, comme d'utiliser d'un téléphone portable, envoyer ou recevoir des messages électroniques, faire des achats en ligne et ainsi de suite. Pour ces applications, la sécurité est une notion cruciale. Par exemple, dans le cas des achats en ligne, il faut que la transaction ait lieu sans divulguer les informations personnelles de l'acheteur à un tiers. Les protocoles de communications contiennent les règles qui régissent ces interactions. Afin de s'assurer qu'ils garantissent un certain niveau de sécurité, on souhaite pouvoir les analyser. Une analyse manuelle, ou leur faire subir des tests, n'est pas suffisant, les attaques pouvant se révéler subtiles. Certains protocols ont été utilisés pendant des années avant qu'une attaque soit découverte contre eux. Étant donnée leur ubiquité croissante dans de nombreuses applications importantes, comme le commerce électronique, un des défis importants auquel la recherche doit faire face consiste à développer des méthodes et des outils de vérification pour augmenter notre confiance dans les protocoles sécurisés, et dans les applications qui dépendent de ces protocoles. Par exemple, plus de 28 milliards d'euros sont dépensés en France au cours de transactions sur Internet, et cette quantité ne cesse d'augmenter. De plus, de nouveaux types de protocoles apparaissent continuellement afin de relever de nouveaux défis technologiques et de société, e.g. le vote électronique, le passeport numérique pour n'en citer que quelques-uns. / With the development of digital networks, such as Internet, communication protocols are omnipresent. Digital devices have to interact with each other in order to perform the numerous and complex tasks we have come to expect as commonplace, such as using a mobile phone, sending or receiving electronic mail, making purchases online and so on. In such applications, security is important. For instance, in the case of an online purchase, the right amount of money has to be paid without leaking the buyer personal information to outside parties. Communication protocols are the rules that govern these interactions. In order to make sure that they guarantee a certainlevel of security, it is desirable to analyze them. Doing so manually or by testing them is not enough, as attacks can be quite subtle. Some protocols have been used for years before an attack was discovered. Because of their increasing ubiquity in many important applications, e.g. electronic commerce, a very important research challenge consists in developing methods and verification tools to increase our trust on security protocols, and so on the applications that rely on them. For example, more than 28 billion Euros were spent in France using Internet transactions, and the number is growing. Moreover, new types of protocols are continuously appearing in order to face new technological and societal challenges, e.g. electronic voting, electronic passport to name a few.

Les neurones biologiques communiquent par le biais d’impulsions électriques, appelées spikes, et les fonctions cérébrales émergent notamment de la coordination entre les réceptions et émissions de ces spikes. Par ailleurs, il est largement admis que la fonction de chaque neurone dépend de sa morphologie. Les dendrites conditionnent l’intégration spatio-temporelle des spikes reçus et influent sur les temps d’occurrence des spikes émis. Elles sont donc fondamentales pour l’étude in silico des mécanismes de coordination, et en particulier pour l’étude des assemblées de neurones. Les modèles de neurones existants prenant en compte les dendrites, sont généralement des modèles mathématiques détaillés, souvent à base d’équations différentielles, dont la simulation nécessite des ressources de calculs importantes. De plus, leur complexité intrinsèque rend difficile l’analyse et les preuves sur ces modèles. Dans cette thèse, nous proposons un modèle de neurone intégrant des dendrites d’une manière abstraite. Dans l’objectif d’ouvrir la porte aux méthodes formelles, nous établissons une définition rigoureuse du cadre de modélisation et mettons en évidence des propriétés algébriques remarquables de l’intégration dendritique. Nous avons notamment démontré qu’il est possible de réduire la structure d’un neurone en préservant sa fonction d’entrée/sortie. Nous avons ainsi révélé des classes d’équivalence dont nous savons déterminer un représentant canonique. En s’appuyant sur la théorie des catégories et par des morphismes de neurones judicieusement définis, nous avons ensuite analysé plus finement ces classes d’équivalence. Un résultat surprenant découle de ces propriétés : un simple ajout de délais dans les modèles informatiques de neurones permet de prendre en compte une intégration dendritique abstraite, sans représenter explicitement la structure arborescente des dendrites. À la racine de l’arborescence dendritique, la modélisation du soma contient inévitablement une équation différentielle lorsque l’on souhaite préserver l’essence du fonctionnement biologique. Ceci impose de combiner une vision analytique avec la vision algébrique. Néanmoins, grâce à une étape préalable de discrétisation temporelle, nous avons également implémenté un neurone complet en Lustre qui est un langage formel autorisant des preuves par model checking. Globalement, nous apportons dans cette thèse un premier pas encourageant vers une formalisation complète des neurones, avec des propriétés remarquables sur l’intégration dendritique. / Biological neurons communicate by means of electrical impulses, called spikes. Brain functions emerge notably from reception and emission coordination between those spikes. Furthermore, it is widely accepted that the function of each neuron depends on its morphology. In particular, dendrites perform the spatio-temporal integration of received spikes and affect the occurrence of emitted spikes. Dendrites are therefore fundamental for in silico studies of coordination mechanisms, and especially for the study of so-called neuron assemblies. Most of existing neuron models taking into account dendrites are detailed mathematical models, usually based on differential equations, whose simulations require significant computing resources. Moreover, their intrinsic complexity makes difficult the analysis and proofs on such models. In this thesis, we propose an abstract neuron model integrating dendrites. In order to pave the way to formal methods, we establish a rigorous definition of the modeling framework and highlight remarkable algebraic properties of dendritic integration. In particular, we have demonstrated that it is possible to reduce a neuron structure while preserving its input/output function. We have thus revealed equivalence classes with a canonical representative. Based on category theory and thanks to properly defined neuron morphisms, we then analyzed these equivalence classes in more details. A surprising result derives from these properties: simply adding delays in neuron computational models is sufficient to represent an abstract dendritic integration, without explicit tree structure representation of dendrites. At the root of the dendritic tree, soma modeling inevitably contains a differential equation in order to preserve the biological functioning essence. This requires combining an analytical vision with the algebraic vision. Nevertheless, thanks to a preliminary step of temporal discretization, we have also implemented a complete neuron in Lustre which is a formal language allowing proofs by model checking. All in all, we bring in this thesis an encouraging first step towards a complete neuron formalization, with remarkable properties on dendritic integration.

Cette thèse développe des outils permettant de prouver qu’un système dynamique est sûr. En supposant qu’une partie de l’espace d’état est dangereuse, un système dynamique est dit sûr lorsque son état n’atteint jamais cette partie dangereuse au cours du temps, quel que soit l’état initial appartenant à un ensemble d’états initiaux admissibles et quel que soit le niveau de perturbation restant dans un domaine admissible. Les outils proposés cherchent à établir des preuves de sûreté pour des systèmes décrits par des modèles dynamiques non-linéaires et des modèles dynamiques hybrides. Prouver qu’un système dynamique est sûr en calculant explicitement l’ensemble des trajectoires possibles du système lorsque le modèle dynamique est non-linéaire et perturbé reste une tâche très difficile. C’est pourquoi cette thèse aborde ce problème à l’aide de fonctions barrières paramétrées. Une barrière, lorsqu’elle existe, permet de partitionner l’espace d’état et d’isoler l’ensemble des trajectoires possibles de l’état du système de la partie dangereuse de l’espace d’état. La fonction paramétrique décrivant la barrière doit satisfaire un certain nombre de contraintes impliquant la dynamique du modèle, l’ensemble des états initiaux possibles, et l’ensemble dangereux. Ces contraintes ne sont pas convexes en général, ce qui complique la recherche de fonctions barrières satisfaisantes. Précédemment, seules des fonctions barrières polynomiales ont été considérées pour des modèles dynamiques polynomiaux. Cette thèse considère des systèmes dynamiques relativement généraux avec des barrières paramétriques quelconques. Les solutions présentées exploitent des outils de satisfaction de contraintes sur des domaines continus et des outils issus de l’analyse par intervalles. Dans un premier temps, cette thèse considère des systèmes dynamiques non-linéaires à temps continu. Le problème de conception d’une barrière paramétrique est formulé comme un problème de satisfaction des contraintes sur des domaines réels avec des variables quantifiées de manière existentielle et universelle. L’algorithme CSC-FPS a été adapté afin de résoudre le problème de synthèse de barrière. Cet algorithme combine une exploration de l’espace des paramètres de la barrière et une phase de vérification des propriétés de la barrière. A l’aide de contracteurs, il est possible de significativement accélérer la recherche de solutions. Dans un second temps, ces résultats sont étendus au cas de systèmes décrits par des modèles dynamiques hybrides. La propriété de sûreté doit être prouvée lors de l’évolution à temps continu du système dynamique, mais aussi pendant les transitions du système. Ceci nécessite l’introduction de contraintes supplémentaires qui lient les fonctions barrières associées à chaque mode à temps continu entre elles. Réaliser la synthèse de toutes les fonctions barrières pour les différents modes simultanément n’est envisageable que pour des systèmes de très petite dimension avec peu de modes. Une approche séquentielle a été proposée. Les contraintes liées aux transitions sont introduites progressivement entre les modes pour lesquels une barrière a déjà été obtenue. Lorsque certaines contraintes de transition ne sont pas satisfaites, une méthode de backtracking doit être mise en œuvre afin de synthétiser des barrières offrant une meilleure prise en compte des contraintes de transition non satisfaites. Ces approches ont été évaluées et comparées avec des techniques de l’état de l’art sur des systèmes décrits par des modèles à temps continu et des modèles hybrides. / This thesis addresses the problem of proving the safety of systems described by non-linear dynamical models and hybrid dynamical models. A system is said to be safe if all trajectories of its state do not reach an unsafe region. Proving the safety of systems by explicitly computing all its trajectories when its dynamic is non-linear or when its behavior is described by an hybrid model with non-linear dynamics remains a challenging task. This thesis considers the barrier function approach to prove the safety of a system. A barrier function, when it exists, partitions the state space and isolates the trajectories of the system starting from any possible initial values of the state and the unsafe part of the state space. The set of constraints, which have to be satisfied by a barrier function are usually non-convex, rendering the search of satisfying barrier functions hard. Previously, only polynomial barrier functions were taken in consideration and for systems with polynomial dynamics. This thesis considers relatively general dynamical systems with generic non-linear barrier functions. The solutions presented are based on template barrier functions, constraint satisfaction problems, and interval analysis. The first part of the thesis focuses on non-linear dynamical systems. The barrier function design problem is formulated as a constraint satisfaction problem that can be solved using tools from interval analysis. This formulation allows one to prove the safety of a non-linear dynamical system by finding the parameters of a template barrier function such that all constraints are satisfied using the FPS-CSC algorithm, which has been adapted and supplemented with contractors to improve its efficiency. The second part of the thesis is dedicated to the design of barrier functions for systems described by hybrid dynamical models. Safety properties have to be proven during the continuous-time evolution of the system, but also during transitions. This leads to additional constraints that have to be satisfied by candidate barrier functions. Solving all the constraints simultaneously to find all the barrier functions is usually computationally intractable. In the proposed approach, the algorithm explores all the locations sequentially. Transition constraints are introduced progressively between the already explored locations. Backtracking to previous location is considered when transition constraints are not satisfied. The efficiency of the proposed approaches has been compared with state-of-the-art solutions.

Cette thèse s'intéresse à quatre projets non construits du groupe d'architectes angeleno Morphosis. Ces quatre projets n'existent que par les maquettes et les dessins qui les représentent, ainsi que par les artefacts conceptuels auxquels ils sont liés ; ils témoignent d'un paroxysme de complexité géométrique et d'un raffinement dans la production graphique, deux caractéristiques du travail des Californiens par lesquelles ils se feront connaître sur la scène internationale à la fin des années 1980. Ces quatre projets – les Malibu, 6th Street, Reno & Was Houses – sont devenus iconiques par la couverture médiatique dont ils ont bénéficié à l'époque, bien que Morphosis les ait présentés sans explications, ou presque. L'ambition de cette recherche est donc de décoder les mécanismes compositionnels et représentationnels à l'oeuvre dans ces projets et dans ces artefacts conceptuels souvent complexes et cryptiques, de façon à exposer les principes à l'oeuvre dans leur écriture architecturale sophistiquée. Pour ce faire, cette recherche dépossède temporairement Morphosis de son statut d'Auteur, et s'empare des objets du corpus afin d'en proposer une lecture interprétative, d'en extirper un propos architectural dont ces objets seraient porteurs, mais que Morphosis n'a jamais explicité comme tel. Les moyens que se donne cette recherche pour mener ces investigations sont principalement des procédés opérationnels basés sur les outils canoniques de la discipline architecturale : la manipulation des systèmes projectifs augmentée des techniques graphiques contemporaines. Il s'agira donc de décrire des objets architecturaux n'existant que dans la représentation graphique, en mobilisant précisément la représentation graphique. Les deux objectifs principaux de cette recherche sont monographiques et méthodologiques. En ce qui concerne les objectifs monographiques, il s'agit de rendre accessible et didactique des procédés de compositions basés sur la systémique et la complexité ostentatoire qui ont fait la marque de fabrique de Morphosis, et de comprendre notamment en quoi les objets du corpus, engendrés par les moyens traditionnels anticipent le courant architectural dit numérique de la décennie qui va suivre. En ce qui concerne les objectifs méthodologiques, il s'agit de mettre au point une méthode d'investigation procédant d'une transposition des outils opérationnels de la conception architecturale dans un contexte analytique ; une méthode faite d'itérations récurrentes empruntant les chemins parfois intuitifs de l'architecte-concepteur, mais dans une démarche d'observation a posteriori, rigoureuse et référencée, en vue de la construction d'un nouveau corpus de connaissances. / Doctorat en Art de bâtir et urbanisme (Architecture) / info:eu-repo/semantics/nonPublished

Cette thèse se positionne dans le domaine de la vérification déductive de programmes, qui consiste à transformer une propriété à vérifier sur un programme en un énoncé logique, pour ensuite démontrer cet énoncé. La vérification effective d'un programme peut poser de nombreuses difficultés pratiques. En fait, les concepts mis en jeu derrière le programme peuvent suffire à faire obstacle à la vérification. En effet, certains programmes peuvent être assez courts et n'utiliser que des constructions simples, et pourtant s'avérer très difficiles à vérifier. Cela nous amène à la question suivante: dans le contexte d'un environnement de vérification déductive de programmes basé sur les démonstrateurs automatiques, quelles méthodes appliquer pour réduire l'effort nécessaire à la fois pour spécifier des comportements attendus complexes, ainsi que pour démontrer qu'un programme respecte ces comportements attendus? Pour mener notre étude, nous nous sommes placés dans le cadre de l'environnement de vérification déductive de programmes Why3. La vérification de programmes en Why3 est basée sur la génération de conditions de vérification, et l'usage de démonstrateurs externes pour les prouver, que ces démonstrateurs soient automatiques ou interactifs. Nous avons développé plusieurs méthodes, certaines générales et d'autres spécifiques à des classes de programmes, pour réduire l'effort manuel. Nos contributions sont les suivantes. Tout d'abord, nous ajoutons des fonctionnalités à Why3 pour assister le processus de vérification, notamment un mécanisme léger de preuve déclarative basé sur la notion d'indicateurs de coupures. Ensuite, nous présentons une méthode de vérification d'absence de débordement arithmétique pour une classe d'utilisation des entiers difficile à traiter par les méthodes standards. Enfin, nous nous intéressons au développement d'une bibliothèque générique pour la spécification et la preuve de programmes générateurs de code. / This thesis is set in the domain of deductive verification of programs, which consists of transforming a property to be verified about a program into a logical statement, and then proving this statement. Effective verification of a program can pose many practical difficulties. In fact, the concepts behind the program may be sufficient to impede verification. Indeed, some programs can be quite short and use only simple constructions, and yet prove very difficult to verify. This leads us to the following question: in the context of a deductive program verification environment based on automatic provers, what methods can be applied to reduce the effort required both to specify complex behaviors, as well as to prove that a program respects these expected behaviors? To carry out our study, we placed ourselves in the context of the deductive verification environment of programs Why3. The verification of programs in Why3 is based on the generation of verification conditions, and the use of external provers to prove them, whether these provers are automatic or interactive. We have developed several methods, some general and others specific to some program classes, to reduce manual effort. Our contributions are as follows. First, we add features to Why3 to assist the verification process, including a lightweight declarative proof mechanism based on the notion of cut indicators. Then we present a method for checking the absence of arithmetic overflow, for use cases which are difficult to process by standard methods. Finally, we are interested in the development of a generic library for the specification and proof of code generating programs.

Cette thèse traite du problème du calcul des implications, c'est-à-dire des régularités de la forme "quand il y a A, il y a B", dans des ensembles de données composés d'objets décrits par des attributs. Calculer toutes les implications peut être vu comme l'énumération d'ensembles d'attributs appelés pseudo-intensions. Nous savons que ces pseudo-intensions ne peuvent pas être énumérées avec un délai polynomial dans l'ordre lectique mais aucun résultat n'existe, à l'heure actuelle, pour d'autres ordres. Bien que certains algorithmes existants n'énumèrent pas forcément dans l'ordre lectique, aucun n'a un délai polynomial. Cette absence de connaissances sur les autres ordres autorise toujours l'existence d'un algorithme avec délai polynomial et le trouver serait une avancée utile et significative. Malheureusement, les algorithmes actuels ne nous autorisent pas à choisir l'ordre d'énumération, ce qui complique considérablement et inutilement l'étude de l'influence de l'ordre dans la complexité. C'est donc pour aller vers une meilleure compréhension du rôle de l'ordre dans l'énumération des pseudo-intensions que nous proposons un algorithme qui peut réaliser cette énumération dans n'importe quel ordre qui respecte la relation d'inclusion. Dans la première partie, nous expliquons et étudions les propriétés de notre algorithme. Comme pour tout algorithme d'énumération, le principal problème est de construire tous les ensembles une seule fois. Nous proposons pour cela d'utiliser un arbre couvrant, lui-même basé sur l'ordre lectique, afin d'éviter de multiples constructions d'un même ensemble. L'utilisation de cet arbre couvrant au lieu de l'ordre lectique classique augmente la complexité spatiale mais offre plus de flexibilité dans l'ordre d'énumération. Nous montrons que, comparé à l'algorithme Next Closure bien connu, le nôtre effectue moins de fermetures logiques sur des contextes peu denses et plus de fermetures quand le nombre moyen d'attributs par objet dépasse 30% du total. La complexité spatiale de l'algorithme est aussi étudiée de façon empirique et il est montré que des ordres différents se comportent différemment, l'ordre lectique étant le plus efficace. Nous postulons que l'efficacité d'un ordre est fonction de sa distance à l'ordre utilisé dans le test de canonicité. Dans la seconde partie, nous nous intéressons au calcul des implications dans un cadre plus complexe : les données relationnelles. Dans ces contextes, les objets sont représentés à la fois par des attributs et par des relations avec d'autres objets. Le besoin de représenter les informations sur les relations produit une augmente exponentielle du nombre d'attributs, ce qui rend les algorithmes classiques rapidement inutilisables. Nous proposons une modification de notre algorithme qui énumère les pseudo-intensions de contextes dans lesquels l'information relationnelle est représentée par des attributs. Nous fournissons une étude rapide du type d'information relationnelle qui peut être prise en compte. Nous utilisons l'exemple des logiques de description comme cadre pour l'expression des données relationnelles. Dans la troisième partie, nous étendons notre travail au domaine plus général des règles d'association. Les règles d'association sont des régularités de la forme ``quand il y a A, il y a B avec une certitude de x%''. Ainsi, les implications sont des règles d'association certaines. Notre algorithme calcule déjà une base pour les implications et nous proposons une très simple modification et montrons qu'elle lui permet de calculer la base de Luxenburger en plus de la base de Duquenne-Guigues. Cela permet à notre algorithme de calculer une base de cardinalité minimale pour les règles d'association. / This thesis deals with the problem of the computation of implications, which are regularities of the form "when there is A there is B", in datasets composed of objects described by attributes. Computing all the implications can be viewed as the enumeration of sets of attributes called pseudo-intents. It is known that pseudointents cannot be enumerated with a polynomial delay in the lectic order but no such result exists for other orders. While some current algorithms do not enumerate in the lectic order, none of them have a polynomial delay. The lack of knowledge on other orders leaves the possibility for a polynomial-delay algorithm to exist and inding it would be an important and useful step. Unfortunately, current algorithms do not allow us to choose the order so studying its inuence on the complexity of the enumeration is harder than necessary. We thus take a first step towards a better understanding of the role of the order in the enumeration of pseudo-intents by providing an algorithm that can enumerate pseudo-intents in any order that respects the inclusion relation.In the first part, we explain and study the properties of our algorithm. As with all enumeration algorithms, the first problem is to construct all the sets only once.We propose to use a spanning tree, itself based on the lectic order, to avoid multiple constructions of a same set. The use of this spanning tree instead of the classic lectic order increases the space complexity but others much more exibility in the enumeration order. We show that, compared to the well-known Next Closure algorithm, ours performs less logical closures on sparse contexts and more once the average number of attributes per object exceeds 30%. The space complexity of the algorithm is also empirically studied and we show that different orders behave differently with the lectic order being the most efficient. We postulate that the efficiency of an order is function of its distance to the order used in the canonicity test. In the second part, we take an interest in the computation of implications in a more complex setting : relational data. In these contexts, objects are represented by both attributes and binary relations with other objects. The need to represent relation information causes an exponential increase in the number of attributes so naive algorithms become unusable extremely fast. We propose a modification of our algorithm that enumerates the pseudo-intents of contexts in which relational information is represented by attributes. A quick study of the type of relational information that can be considered is provided. We use the example of description logics as a framework for expressing relational data. In the third part, we extend our work to the more general domain of association rules. Association rules are regularities of the form \when there is A there is B with x% certainty" so implications are association rules with 100% certainty. Our algorithm already computes a basis for implications so we propose a very simple modification and demonstrate that it can compute the Luxenburger basis of a context along with the Duquenne-Guigues basis. This effectively allows our algorithm to compute a basis for association rules that is of minimal cardinality.

La prise de conscience générale de l'importance de vérifier plus scrupuleusement les programmes a engendré une croissance considérable des efforts de vérification formelle de programme durant cette dernière décennie. Néanmoins, le code qu'exécute l'ordinateur, ou code exécutable, n'est pas le code écrit par le développeur, ou code source. La vérification formelle de compilateurs est donc un complément indispensable à la vérification de code source.L'une des tâches les plus complexes de compilation est l'allocation de registres. C'est lors de celle-ci que le compilateur décide de la façon dont les variables du programme sont stockées en mémoire durant son exécution. La mémoire comporte deux types de conteneurs : les registres, zones d'accès rapide, présents en nombre limité, et la pile, de capacité supposée suffisamment importante pour héberger toutes les variables d'un programme, mais à laquelle l'accès est bien plus lent. Le but de l'allocation de registres est de tirer au mieux parti de la rapidité des registres, car une allocation de registres de bonne qualité peut conduire à une amélioration significative du temps d'exécution du programme.Le modèle le plus connu de l'allocation de registres repose sur la coloration de graphe d'interférence-affinité. Dans cette thèse, l'objectif est double : d'une part vérifier formellement des algorithmes connus d'allocation de registres par coloration de graphe, et d'autre part définir de nouveaux algorithmes optimisants pour cette étape de compilation. Nous montrons tout d'abord que l'assistant à la preuve Coq est adéquat à la formalisation d'algorithmes d'allocation de registres par coloration de graphes. Nous procédons ainsi à la vérification formelle en Coq d'un des algorithmes les plus classiques d'allocation de registres par coloration de graphes, l'Iterated Register Coalescing (IRC), et d'une généralisation de celui-ci permettant à un utilisateur peu familier du système Coq d'implanter facilement sa propre variante de cet algorithme au seul prix d'une éventuelle perte d'efficacité algorithmique. Ces formalisations nécessitent des réflexions autour de la formalisation des graphes d'interférence-affinité, de la traduction sous forme purement fonctionnelle d'algorithmes impératifs et de l'efficacité algorithmique, la terminaison et la correction de cette version fonctionnelle. Notre implantation formellement vérifiée de l'IRC a été intégrée à un prototype du compilateur CompCert.Nous avons ensuite étudié deux représentations intermédiaires de programmes, dont la forme SSA, et exploité leurs propriétés pour proposer de nouvelles approches de résolution optimale de la fusion, l'une des optimisations opéréeslors de l'allocation de registres dont l'impact est le plus fort sur la qualité du code compilé. Ces approches montrent que des critères de fusion tenant compte de paramètres globaux du graphe d'interférence-affinité, tels que sa largeur d'arbre, ouvrent la voie vers de nouvelles méthodes de résolution potentiellement plus performantes. / The need for trustful programs led to an increasing use of formal verication techniques the last decade, and especially of program proof. However, the code running on the computer is not the source code, i.e. the one written by the developper, since it has to betranslated by the compiler. As a result, the formal verication of compilers is required to complete the source code verication. One of the hardest phases of compilation is register allocation. Register allocation is the phase within which the compiler decides where the variables of the program are stored in the memory during its execution. The are two kinds of memory locations : a limited number of fast-access zones, called registers, and a very large but slow-access stack. The aim of register allocation is then to make a great use of registers, leading to a faster runnable code.The most used model for register allocation is the interference graph coloring one. In this thesis, our objective is twofold : first, formally verifying some well-known interference graph coloring algorithms for register allocation and, second, designing new graph-coloring register allocation algorithms. More precisely, we provide a fully formally veri ed implementation of the Iterated Register Coalescing, a very classical graph-coloring register allocation heuristics, that has been integrated into the CompCert compiler. We also studied two intermediate representations of programs used in compilers, and in particular the SSA form to design new algorithms, using global properties of the graph rather than local criteria currently used in the litterature.