La sécurité des applications sur le web est totalement dépendante de leur design et de la robustesse de l'implémentation des algorithmes et protocoles cryptographiques sur lesquels elles s'appuient. Cette thèse présente une nouvelle approche, applicable à de larges projets, pour vérifier l'état de l'art des algorithmes de calculs sur les grands nombres, tel que rencontrés dans les implémentations de référence. Le code et les preuves sont réalisés en F*, un langage orienté preuve et qui offre un système de types riche et expressif. L'implémentation et la vérification dans un langage d'ordre supérieur permet de maximiser le partage de code mais nuit aux performances. Nous proposons donc un nouveau langage, Low*, qui encapsule un sous ensemble de C en F* et qui compile vers C de façon sûre. Low* conserve toute l'expressivité de F* pour les spécifications et les preuves et nous l'utilisons pour implémenter de la cryptographie, en y intégrant les optimisations des implémentations de référence. Nous vérifions ce code en termes de sûreté mémoire, de correction fonctionnelle et d'indépendance des traces d'exécution vis à vis des données sensibles. Ainsi, nous présentons HACL*, une bibliothèque cryptographique autonome et entièrement vérifiée, dont les performances sont comparables sinon meilleures que celles du code C de référence. Plusieurs algorithmes de HACL* font maintenant partie de la bibliothèque NSS de Mozilla, utilisée notamment dans Firefox et dans RedHat. Nous appliquons les mêmes concepts sur miTLS, une implémentation de TLS vérifiée et montrons comment étendre cette méthodologie à des preuves cryptographiques, du parsing de message et une machine à état. / The security of Internet applications relies crucially on the secure design and robust implementations of cryptographic algorithms and protocols. This thesis presents a new, scalable and extensible approach for verifying state-of-the-art bignum algorithms, found in popular cryptographic implementations. Our code and proofs are written in F∗, a proof-oriented language which offers a very rich and expressive type system. The natural way of writing and verifying higher-order functional code in F∗ prioritizes code sharing and proof composition, but this results in low performance for cryptographic code. We propose a new language, Low∗, a fragment of F∗ which can be seen as a shallow embedding of C in F∗ and safely compiled to C code. Nonetheless, Low∗ retains the full expressiveness and verification power of the F∗ system, at the specification and proof level. We use Low∗ to implement cryptographic code, incorporating state-of-the-art optimizations from existing C libraries. We use F∗ to verify this code for functional correctness, memory safety and secret in- dependence. We present HACL∗, a full-fledged and fully verified cryptographic library which boasts performance on par, if not better, with the reference C code. Several algorithms from HACL∗ are now part of NSS, Mozilla’s cryptographic library, notably used in the Firefox web browser and the Red Hat operating system. Eventually, we apply our techniques to miTLS, a verified implementation of the Transport Layer Security protocol. We show how they extend to cryptographic proofs, state-machine implementations and message parsing verification.

Dans une démarche classique d'ingénierie dirigée par les modèles (IDM), l'ingénieur modélise son système à l'aide d'une notation semi-formelle, le valide puis l'implante. L'étape de validation, basée sur ces modèles, est particulièrement cruciale pour les systèmes temps-réel répartis et embarqués (TR2E), afin de s'assurer de leur respect d'invariants de sécurité, ou de leur bon fonctionnement logique ou temporel. Cependant, une démarche IDM n'est pas suffisante car elle n'indique pas comment utiliser les modèles pour faire des analyses. Quels modèles (ou vues) utiliser ? Pour analyser quel type de propriétés ? Ainsi, il est nécessaire d'adopter une démarche d'Ingénierie dirigée par les Vérifications et les Validations (IDV2) : les modèles créés sont ceux qui sont utiles pour s'assurer que le système est correctement construit (vérification), et qu'il satisfait un ensemble de propriétés spécifiées en amont dans le processus de développement (validation). Cette thèse propose un processus de développement, de validation et de vérification basé sur des notations formelles, et dédié aux applications temps-réel réparties embarquées. Nous nous appuyons sur une notation pivot standard pour appliquer cette démarche IDV2 : le langage AADL (Architecture Analysis and Design Language) permet à l'ingénieur de spécifier son application TR2E depuis son architecture matérielle jusqu'à son déploiement logiciel. Il repose sur l'existence d'un exécutif ayant certaines propriétés et proposant différents services. Ce processus prend en compte les aspects comportementaux de l'application ainsi que les aspects architecturaux de l'exécutif. Il repose sur des notations standardisées, permettant de faire face aux problèmes d'interopérabilités des outils mis en oeuvre. Pour l'applicatif, des propriétés comme l'absence d'interblocage, l'utilisation et le dimensionnement de ressources ou encore l'ordonnancement du système sont validées. Pour l'exécutif, le fait que l'architecture de celui-ci et les services proposés sont en adéquation avec les propriétés évoquées lors de sa configuration est vérifié. Notre démarche permet d'obtenir des retours aussi bien à propos de l'applicatif que de l'exécutif, et permet de corriger ou modifier les modèles dans un processus de développement itératif. Au cours de notre démarche, nous exploitons et transformons les spécifications AADL vers différentes notations standardisées : les réseaux de Petri pour la validation de l'applicatif, la notation Z pour la vérification de l'exécutif utilisé, PolyORB.

Dans cette thèse nous proposons un cadre formel complet pour l'analyse des systèmes temporisés, avec l'accent mis sur la valeur pratique de l'approche. Nous décrivons des systèmes comme des automates temporisés et nous exprimons les propriétés en logiques temps-réel. Nous considérons deux types d'analyse. Vérification : étant donnés un système et une propriété, vérifier que le système satisfait la propriété. Synthèse de contrôleurs : étant donnés un système et une propriété, restreindre le système pour qu'il satisfasse la propriété. Pour rendre l'approche possible malgré la difficulté théorique des problèmes, nous proposons : Des abstractions pour réduire l'espace d'états concret en un espace abstrait beaucoup plus petit qui, pourtant, préserve toutes les propriétés qui nous intéressent. Des techniques efficaces pour calculer et explorer l'espace d'états abstrait. Nous définissons des bisimulations et simulations faisant abstraction du temps et nous étudions les propriétés qu'elles préservent. Pour les bisimulations, l'analyse consiste à générer d'abord l'espace abstrait, et ensuite l'utiliser pour vérifier des propriétés sur l'espace concret. Pour les simulations, la génération et la vérification se font en même temps (à-la-volée). Un algorithme à-la-volée est aussi développé pour la synthèse de contrôleurs. Pour aider l'utilisateur à sa compréhension du système, nous produisons des séquences diagnostiques concrètes. Nous avons implanté nos méthodes dans Kronos, l'outil d'analyse temps-réel de Verimag, et nous avons traité un nombre d'études de cas réalistes parmi lesquelles le protocole FRP-DT de réservation rapide de débit pour les réseaux ATM (dans le cadre d'une coopération scientifique avec le CNET), le protocole de détection de collisions dans un réseaux à accès multiple de Band&Olufsen, l'ordonnancement de tâches temps-réel périodiques, la cohérence et l'ordonnancement des documents multimédia, ainsi qu'un nombre d'études de cas benchmarks, telles que le protocole d'exclusion mutuelle de Fischer, les protocoles de communication CSMA/CD et FDDI.

Cette thèse propose une analyse du développement économique à partir du concept de facteur humain qui apparaît en économie institutionnelle à travers les institutions informelles. Ces dernières sont responsables du caractère spécifique de chaque structure institutionnelle nationale qui forme le cadre incitatif de l'économie. Composée de règles formelles et informelles, la structure institutionnelle représente un ensemble évolutif. L'objectif élargi de cette recherche est donc de comprendre l'évolution et le changement des structures institutionnelles en étudiant particulièrement l'impact international sur ce processus. L'objectif spécifique de ce travail est d'appliquer l'approche développée au cas de la Russie afin de contribuer à une meilleure compréhension de la structure institutionnelle russe actuelle, de son efficacité pour le développement économique du pays et de l'impact de l'ouverture économique sur son changement, et notamment sur le facteur humain russe. Avec l'adhésion de la Russie en 2012 à l'Organisation Mondiale du Commerce cette question est d'intérêt particulier car le pays s'ouvre aux nouveaux attributs de la mondialisation. En mobilisant le cadre théorique croisé entre l'économie institutionnelle, l'économie de développement et l'économie internationale, cette étude nous conduit à présenter la mondialisation en tant que processus institutionnel qui en généralisant les institutions formelles de l'économie de marché et de la démocratie à l'échelle planétaire, a ignoré le rôle du facteur humain local. Cela explique la différence des performances économiques des pays qui ont adopté les mêmes cadres organisationnels. En revanche, la prise en considération du facteur humain dans l'analyse économique permet de développer la vision plus optimiste de la mondialisation. En facilitant le contact direct entre les représentants des structures institutionnelles différentes, elle est capable de stimuler l'évolution des normes de comportement improductif vers les valeurs sociales incitant les actions productives. En appliquant ce constat à l'analyse de la structure institutionnelle russe qui a vu diverger ses institutions formelles et informelles en résultat des réformes de la transition des années 1990, il est possible de conclure que l'ouverture économique de ce pays dans les conditions actuelles favorisera le changement de son facteur humain. Compte tenu de l'incohérence entre le cadre formel et les institutions informelles russes, l'évolution de ces dernières contribuera à l'instauration de l'ordre social formel et impersonnel.

Dans cette thèse, nous nous intéressons à la spécification et à la synthèse de contrôleurs des systèmes temps-réels. Les modèles pour ces systèmes sont des Event-recording Automata. Nous supposons que les contrôleurs observent tous les évènements se produisant dans le système et qu'ils peuvent interdirent uniquement des évènements contrôlables. Tous les évènements ne sont pas nécessairement contrôlables. Une première étude est faite sur la logique Event-recording Logic (ERL). Nous proposons des nouveaux algorithmes pour les problèmes de vérification et de satisfaisabilité. Ces algorithmes présentent les similitudes entre les problèmes de décision cité ci-dessus et les problèmes de décision similaires étudiés dans le cadre du $\mu$-calcul. Nos algorithmes corrigent aussi des algorithmes présents dans la littérature. Les similitudes relevées nous permettent de prouver l'équivalence entre les formules de ERL et les formules de ERL en forme normale disjonctive. La logique ERL n'étant pas suffisamment expressive pour décrire certaines propriétés des systèmes, en particulier des propriétés des contrôleurs, nous introduisons une nouvelle logique WT$_\mu$. La logique WT$_\mu$ est une extension temps-réel faible du $\mu$-calcul. Nous proposons des algorithmes pour la vérification des systèmes lorsque les propriétés sont écrites en WT$_\mu$. Nous identifions deux fragments de WT$_\mu$ appelés WT$_\mu$ bien guardé ($WG$-WT$_\mu$) et WT$_\mu$ pour le contrôle ($C$-WT$_\mu$). La logique $WG$-WT$_\mu$ est plus expressif que $C$-WT$_\mu$. Nous proposons un algorithme qui permet de vérifier si une formule de $WG$-WT$_\mu$ possède un modèle (éventuellement déterministe). Cet algorithme nécessite de connaître les ressources (horloges et constante maximale comparée avec les horloges) des modèles. Dans le cadre de $C$-WT$_\mu$ l'algorithme que nous proposons et qui permet de décider si une formule possède un modèle n'a pas besoin de connaître les ressources des modèles. En utilisant $C$-WT$_\mu$ comme langage de spécification des systèmes, nous proposons des algorithmes de décision pour le contrôle centralisé et le $\Delta$-contrôle centralisé. Ces algorithmes permettent aussi de construire des modèles de contr\^oleurs. Lorsque les objectifs de contrôle sont décrits à l'aide des formules de $WG$-WT$_\mu$, nous montrons également comment synthétiser des contrôleurs décentralisés avec des ressources fixées à l'avance et ceci, lorsqu'au plus un contrôleur est non déterministe. / In this dissertation, we consider the specification and the controller synthesis problem for real-time systems. Our models for systems are kinds of Event-recording automata. We assume that controllers observe all the events occurring in the system and can prevent occurrences of controllable events. We study Event-recording Logic (ERL). We propose new algorithms for the model-checking and the satisfiability problems of that logic. Our algorithms are similar to some algorithms proposed for the same problems in the setting of the standard $\mu$-calculus. They also correct earlier proposed algorithms. We define disjunctive normal form formulas and we show that every formula is equivalent to a formula in disjunctive normal form. Unfortunately, ERL is rather weak and can not describe some interesting real-time properties, in particular some important properties for controllers. We define a new logic that we call WT$_\mu$. The logic WT$_\mu$ is a weak real-time extension of the standard $\mu$-calculus. We present an algorithm for the model-checking problem of WT$_\mu$. We consider two fragments of WT$_\mu$ called well guarded WT$_\mu$ ($WG$-WT$_\mu$) and WT$_\mu$ for control ($C$-WT$_\mu$). We show that the satisfiability of $WG$-WT$_\mu$ is decidable if the maximal constants appearing in models are known a priori. Our algorithm allows to check whether a formula of $WG$-WT$_\mu$ has a deterministic model. The algorithm we propose to decide whether a formula of $C$-WT$_\mu$ has a model does not need to know the maximal constant used in models. All the algorithms for the satisfiability checking construct witness models. Using $C$-WT$_\mu$, we present algorithms for a centralised controller synthesis problem and a centralised $\Delta$-controller synthesis problems. The construction of witness controllers is effective. We also consider the decentralised controller synthesis problem with limited resources (the maximal constants used in controllers is known a priory) when the properties are described with $WG$-WT$_\mu$. We show that this problem is decidable and the computation of witness controllers is effective.

La recherche de règles d’association intéressantes est un domaine important et actif en fouille de données. Puisque les algorithmes utilisés en extraction de connaissances à partir de données (ECD), ont tendance à générer un nombre important de règles, il est difficile à l’utilisateur de sélectionner par lui même les connaissances réellement intéressantes. Pour répondre à ce problème, un post-filtrage automatique des règles s’avère essentiel pour réduire fortement leur nombre. D’où la proposition de nombreuses mesures d’intérêt dans la littérature, parmi lesquelles l’utilisateur est supposé choisir celle qui est la plus appropriée à ses objectifs. Comme l’intérêt dépend à la fois des préférences de l’utilisateur et des données, les mesures ont été répertoriées en deux catégories : les mesures subjectives (orientées utilisateur ) et les mesures objectives (orientées données). Nous nous focalisons sur l’étude des mesures objectives. Néanmoins, il existe une pléthore de mesures objectives dans la littérature, ce qui ne facilite pas le ou les choix de l’utilisateur. Ainsi, notre objectif est d’aider l’utilisateur, dans sa problématique de sélection de mesures objectives, par une approche par catégorisation. La thèse développe deux approches pour assister l’utilisateur dans sa problématique de choix de mesures objectives : (1) étude formelle suite à la définition d’un ensemble de propriétés de mesures qui conduisent à une bonne évaluation de celles-ci ; (2) étude expérimentale du comportement des différentes mesures d’intérêt à partir du point de vue d’analyse de données. Pour ce qui concerne la première approche, nous réalisons une étude théorique approfondie d’un grand nombre de mesures selon plusieurs propriétés formelles. Pour ce faire, nous proposons tout d’abord une formalisation de ces propriétés afin de lever toute ambiguïté sur celles-ci. Ensuite, nous étudions, pour différentes mesures d’intérêt objectives, la présence ou l’absence de propriétés caractéristiques appropriées. L’évaluation des mesures est alors un point de départ pour une catégorisation de celle-ci. Différentes méthodes de classification ont été appliquées : (i) méthodes sans recouvrement (CAH et k-moyennes) qui permettent l’obtention de groupes de mesures disjoints, (ii) méthode avec recouvrement (analyse factorielle booléenne) qui permet d’obtenir des groupes de mesures qui se chevauchent. Pour ce qui concerne la seconde approche, nous proposons une étude empirique du comportement d’une soixantaine de mesures sur des jeux de données de nature différente. Ainsi, nous proposons une méthodologie expérimentale, où nous cherchons à identifier les groupes de mesures qui possèdent, empiriquement, un comportement semblable. Nous effectuons par la suite une confrontation avec les deux résultats de classification, formel et empirique dans le but de valider et mettre en valeur notre première approche. Les deux approches sont complémentaires, dans l’optique d’aider l’utilisateur à effectuer le bon choix de la mesure d’intérêt adaptée à son application. / The search for interesting association rules is an important and active field in data mining. Since knowledge discovery from databases used algorithms (KDD) tend to generate a large number of rules, it is difficult for the user to select by himself the really interesting knowledge. To address this problem, an automatic post-filtering rules is essential to significantly reduce their number. Hence, many interestingness measures have been proposed in the literature in order to filter and/or sort discovered rules. As interestingness depends on both user preferences and data, interestingness measures were classified into two categories : subjective measures (user-driven) and objective measures (data-driven). We focus on the study of objective measures. Nevertheless, there are a plethora of objective measures in the literature, which increase the user’s difficulty for choosing the appropriate measure. Thus, our goal is to avoid such difficulty by proposing groups of similar measures by means of categorization approaches. The thesis presents two approaches to assist the user in his problematic of objective measures choice : (1) formal study as per the definition of a set of measures properties that lead to a good measure evaluation ; (2) experimental study of the behavior of various interestingness measures from data analysispoint of view. Regarding the first approach, we perform a thorough theoretical study of a large number of measures in several formal properties. To do this, we offer first of all a formalization of these properties in order to remove any ambiguity about them. We then study for various objective interestingness measures, the presence or absence of appropriate characteristic properties. Interestingness measures evaluation is therefore a starting point for measures categorization. Different clustering methods have been applied : (i) non overlapping methods (CAH and k-means) which allow to obtain disjoint groups of measures, (ii) overlapping method (Boolean factor analysis) that provides overlapping groups of measures. Regarding the second approach, we propose an empirical study of the behavior of about sixty measures on datasets with different nature. Thus, we propose an experimental methodology, from which we seek to identify groups of measures that have empirically similar behavior. We do next confrontation with the two classification results, formal and empirical in order to validate and enhance our first approach. Both approaches are complementary, in order to help the user making the right choice of the appropriate interestingness measure to his application.

Dans cette thèse, nous avons étudié et développé un environnement de preuve pour les algorithmes distribués. Nous avons choisi de combiner d’une part l’approche "correct-par-construction" basée sur la méthode "B évènementielle" et d’autre part les calculs locaux comme un outil de codage et de preuve d’algorithmes distribués. Ainsi, nous avons proposé un patron et une approche qui caractérisent d’une façon incrémentale une démarche générale de preuve de plusieurs classes d’algorithmes distribués. Les solutions proposées sont validées et implémentées par un outil de preuve appelé B2Visidia. / In this thesis, we have studied and developed a proof environment for distributed algorithms. We have chosen to combine the “correct-by-construction” approach based on the “Event-B” method and the local computations models. These models define abstract computing processes for solving problems by distributed algorithms. Thus, we have proposed a pattern and an approach to characterize a general approach to prove several classes of distributed algorithms. The proposed solutions are implemented by a tool called B2Visidia.

Nous avons dans cette thèse cherché à définir un formalisme simple pour pouvoir modéliser des systèmes où se combinent des phénomènes non-déterministes et des comportements aléatoires. Nous avons choisi d'étendre le formalisme de la réécriture pour lui permettre d'exprimer des phénomènes probabilistes, puis nous avons étudié la terminaison en temps moyen fini de ce modèle. Nous avons également présenté une notion de stratégie pour contrôler l'application des règles de réécriture probabilistes et nous présentons des critères généraux permettant d'identifier des classes de stratégies sous lesquelles les systèmes de réécriture probabilistes terminent en temps moyen fini. Afin de mettre en valeur notre formalisme et les méthodes de preuve de terminaison en temps moyen fini, nous avons modélisé un réseau de stations \WIFI~ et nous montrons que toutes les stations parviennent à émettre leurs messages dans un temps moyen fini. / In this thesis we define a new formalism that allows to model transition systems where transitions can be either probabilistic or non deterministic. We choose to extend the rewriting formalism because it allows to simply express non-deterministic behavior. Latter, we study the termination of such systems and we give some criteria that imply the termination within a finite mean number of rewrite steps. We also study the termination of such systems when the firing of probabilistic rules are controlled by strategies. In this document, we use our techniques to model the \WIFI~ protocol and show that a pool of stations successfully emits all its messages within a finite mean time.

Cette thèse propose une analyse du développement économique à partir du concept de facteur humain qui apparaît en économie institutionnelle à travers les institutions informelles. Ces dernières sont responsables du caractère spécifique de chaque structure institutionnelle nationale qui forme le cadre incitatif de l'économie. Composée de règles formelles et informelles, la structure institutionnelle représente un ensemble évolutif. L'objectif élargi de cette recherche est donc de comprendre l'évolution et le changement des structures institutionnelles en étudiant particulièrement l'impact international sur ce processus. L'objectif spécifique de ce travail est d'appliquer l'approche développée au cas de la Russie afin de contribuer à une meilleure compréhension de la structure institutionnelle russe actuelle, de son efficacité pour le développement économique du pays et de l'impact de l'ouverture économique sur son changement, et notamment sur le facteur humain russe. Avec l'adhésion de la Russie en 2012 à l'Organisation Mondiale du Commerce cette question est d'intérêt particulier car le pays s'ouvre aux nouveaux attributs de la mondialisation. En mobilisant le cadre théorique croisé entre l'économie institutionnelle, l'économie de développement et l'économie internationale, cette étude nous conduit à présenter la mondialisation en tant que processus institutionnel qui en généralisant les institutions formelles de l'économie de marché et de la démocratie à l'échelle planétaire, a ignoré le rôle du facteur humain local. Cela explique la différence des performances économiques des pays qui ont adopté les mêmes cadres organisationnels. En revanche, la prise en considération du facteur humain dans l'analyse économique permet de développer la vision plus optimiste de la mondialisation. En facilitant le contact direct entre les représentants des structures institutionnelles différentes, elle est capable de stimuler l'évolution des normes de comportement improductif vers les valeurs sociales incitant les actions productives. En appliquant ce constat à l'analyse de la structure institutionnelle russe qui a vu diverger ses institutions formelles et informelles en résultat des réformes de la transition des années 1990, il est possible de conclure que l'ouverture économique de ce pays dans les conditions actuelles favorisera le changement de son facteur humain. Compte tenu de l'incohérence entre le cadre formel et les institutions informelles russes, l'évolution de ces dernières contribuera à l'instauration de l'ordre social formel et impersonnel. / This PhD dissertation analyzes the economic development from the concept of human factor which appears in the Institutional Economics trough the informal institutions. These institutions are responsible for the specific character of each national institutional structure which forms the incentive system of an economy. An institutional framework as a composite of formal rules and informal institutions is an evolutionary set. The wider objective of this thesis is to understand the evolution and change of institutional structures by studying in particular the international impact on this process. The specific objective of this research work is to apply the developed approach to the Russian case in order to better understand the actual Russian institutional structure, its effectiveness for the economic development of the country and the impact of the economic openness on the institutional change, in particular on the Russian human factor. This impact is a highly topical question for Russia because of its greater economic openness due to its accession to the World Trade Organization completed in 2012. Within the theoretical framework formed by Institutional Economics, Development Economics and International Economics, this research leads us to present the globalization as an institutional process which generalized formal institutions of the market economy and the democracy on the global scale but which ignored the role of the local human factor. It explains the differences of the economic performance in the countries who adopted the same formal framework. In contrast, taking into account the role of the human factor in the economic development allows to develop more optimistic views of globalization. By facilitating the direct contact between the representatives of the different institutional structures, the globalization can stimulate the evolution of social norms of unproductive behavior to the social values inciting productive actions. Applying this to the Russian framework which formal and informal institutions became strongly divergent in result of the transition reforms of 1990s, it is possible to conclude that the economic openness of this country in the actual situation will favor the change of its human factor. Considering the incoherence between Russian actual formal framework and Russian informal institutions, the evolution of the last will contribute to establish former and impersonal social order.

La présente thèse porte sur le développement d'une théorie d'algèbre linéaire, de géométrie et d'analyse basée sur les algèbres (Z2)n-commutatives, c'est-à-dire des algèbres (Z2)n-graduées associatives unitaires satisfaisant ab = (-1)<deg(a),deg(b)>ba, pour tout couple d'éléments homogènes a, b de degrés deg(a), deg(b) où <.,.> est le produit scalaire usuel). Cette généralisation de la supergéométrie a de nombreuses applications : en mathématiques (l'algèbre de Deligne des superformes différentielles, l'algèbre des quaternions et les algèbres de Clifford en sont des exemples) et même en physique (paraparticules). Dans ce travail, les notions de trace et de (super)déterminant pour des matrices à coefficients dans une algèbre gradué-commutative sont définies et étudiés. Une attention particulière est portée au cas des algèbres de Clifford : ce point de vue gradué fournit une nouvelle approche au problème classique du « bon » déterminant pour des matrices à coefficient non-commutatifs (quaternioniques). En outre, nous entreprenons l'étude de la géométrie différentielle (Z2)n-graduée. Privilégiant l'approche par les espaces annelés, les (Z2)n-supervariétés sont définies en choisissant l'algèbre (Z2)n-commutative des séries formelles en variables graduées comme modèle pour le faisceau de fonctions. Les résultats les plus marquants ainsi obtenus sont : le Berezinien gradué et son interprétation cohomologique (essentielle pour établir une théorie de l'intégration) ; le théorème des morphismes, attestant qu'on peut rétablir un morphisme entre (Z2)n-supervariétés à partir de sa seule expression sur les coordonnées ; le théorème de Batchelor-Gawedzki pour les (Z2)n-supervariétés lisses / The present thesis deals with a development of linear algebra, geometry and analysis based on (Z2)n-superalgebras ; associative unital algebras which are (Z2)n-graded and graded-commutative, i.e. statisfying ab=(-1)<deg(a),deg(b)>ba, for all homogeneous elements a, b of respective degrees deg(a), deg(b) in (Z2)n (<.,.> denoting the usual scalar product). This generalization widens the range of applications of supergeometry to many mathematical structures (quaternions and more generally Clifford algebras, Deligne algebra of superdifferential forms, higher vector bundles) and appears also in physics (for describing paraparticles) proving its worth and relevance. In this dissertation, we first focus on (Z2)n-superalgebra theory ; we define and characterize the notions of trace and (super)determinant of matrices over graded-commutative algebras. Special attention is given to the case of Clifford algebras, where our study gives a new approach to treat the classical problem of finding a “good” determinant for matrices with noncommuting (quaternionic) entries. Further, we undertake the study of (Z2)n-graded differential geometry. Privileging the ringed space approach, we define (smooth) (Z2)n-supermanifolds modeling their algebras of functions on the (Z2)n-commutative algebra of formal power series in graded variables, and develop the theory along the lines of supergeometry. Notable results are : the graded Berezinian and its cohomological interpretation (essential to establish integration theory) ; the theorem of morphism, which states that a morphism of (Z2)n-supermanifolds can be recovered from its coordinate expression ; Batchelor-Gawedzki theorem for (Z2)n-supermanifolds