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.

Les systèmes réactifs sont modélisés avec différents types d'automates, tels que les systèmes de transitions symboliques à entrée sortie (IOSTS). L'exécution symbolique d'un IOSTS permet la génération de cas de test qui peuvent être exécutés sur une implantation concrète, afin de déterminer si elle est conforme à son modèle. Dans ce document, nous étendons les IOSTS avec des appels de fonctions utilisateur et analysons leur impact sur le système entier et viceversa. Cette thèse comble l'écart entre une approche basée sur le modèle où les fonctions utilisateur sont abstraites et une approche basée sur le code où les petits morceaux de code sont considérés séparément, indépendamment de la façon dont ils sont combinés. Selon le niveau de connaissance que nous avons sur ces fonctions, elles sont modélisées soit par une spécification complète, soit par une spécification partielle, soit juste comme des boîtes noires fournies sans aucune connaissance. Premièrement, lorsque les fonctions sont partiellement connues, nous utilisons des bouchons définis par des tables contenant des tuples représentatifs des données d'entrée/sortie. L'approche proposée emprunte au test "concolic", l'idée de mélanger l'exécution symbolique avec l'information obtenue à partir d'exécutions concrètes des fonctions (tables). Deuxièmement, si l'utilisateur est prêt à fournir d'autres spécifications, il serait intéressant d'utiliser des représentations plus complètes pour les fonctions. Par conséquent, nous proposons d'abstraire des comportements des fonctions par des contrats pré/post. Ensuite, nous étendons l'exécution symbolique en analysant les fonctions via leurs contrats. Enfin, lorsque les fonctions appelées sont complètement inconnues, nous présentons une approche pour extraire de nouveaux contrats pour eux en explorant les contraintes issues de l'exécution symbolique de l'IOSTS. De tels contrats reflètent les contraintes des fonctions qui rendent possible un certain comportement (exigence). / Reactive systems are modeled with various kinds of automata, such as Input Output Symbolic Transition Systems (IOSTS). Symbolic execution over an IOSTS allows test cases generation that can be executed on a concrete implementation, in order to determine whether it is conforming to its model. In this dissertation, we aim at extending the IOSTS framework with explicit user-defined function calls and analyze their impact on a whole system and vice-versa. The thesis bridges the gap between a model-based approach in which user-defined functions are abstracted away and a code-based approach in which small pieces of code are considered separately regardless of the way they are combined. According to the level of knowledge we have about these functions, they are modeled either by a complete specification, a partial specification, or even just as black-boxes provided without any knowledge. First, when functions are partially known, we use function stubs defined by tables containing representative input/output data tuples. The proposed approach borrows from concolic testing, the idea of mixing symbolic execution with information obtained from instrumented concrete executions (function tables). Second, if the user is willing to provide further specifications, it would be interesting to use more complete representations for called functions. Hence, we propose to abstract function behaviors by means of pre/post contracts. Then we extend symbolic execution by analyzing the functions through their contracts. Finally, when called functions are completely unknown, we present an approach to extract new contracts for them by exploring constraints coming from the IOSTS symbolic execution. Such contracts reflect constraints on the functions that make some behavior (requirement) feasible.

Cette thèse s'inscrit dans le domaine de la vérification de protocoles cryptographiques dans le modèle symbolique. Plus précisément, il s'agit de s'assurer à l'aide de méthodes formelles que de petits programmes distribués satisfont à des propriétés d'indistinguabilité, c'est-à-dire qu'un attaquant n'est pas capable de deviner quelle situation (parmi deux)il observe. Ce formalisme permet d'exprimer des propriétés de sécurité comme le secret fort, l'intraçabilité ou l'anonymat. De plus, les protocoles sont exécutés simultanément par un grand nombre d'agents, à plusieurs reprises si bien que nous nous heurtons très rapidement à des résultats d'indécidabilité. Dès lors, il faut ou bien tenir compte du nombre arbitraire de sessions et rechercher des méthodes de semi-décision ou identifier des classes décidables ;ou bien établir des procédures de décision pour un nombre fini de sessions. Au moment où nous avons commencé les travaux présentés dans cette thèse les outils de vérification de propriétés d'indistinguabilité pour un nombre borné de sessions ne permettaient de traiter que très peu de sessions :dans certains cas il était tout juste possible de modéliser un échange complet. Cette thèse présente des procédures de décision efficaces dans ce cadre. Dans un premier temps, nous établissons des résultats de petite attaque. Pour des protocoles déterministes nous démontrons qu'il existe une attaque si, et seulement s’il existe une attaque bien typée lorsque toute confusion entre les types des variables est évitée. De plus, nous prouvons que, lorqu'il existe une attaque l'attaquant peut la trouver en utilisant au plus trois constantes. Dans un second temps, nous traduisons le problème d'indistinguabilité en termes d'accessibilité dans un système de planification qui est résolu par l'algorithme du graphe de planification associé à un codage SAT. Nous terminons en confirmant l'efficacité de la démarche ,à travers l'implémentation de l'outil SAT-Equivet sa comparaison vis-à-vis des outils analogues. / This thesis presents methods to verify cryptographic protocolsin the symbolic model: formal methods allowto verify that small distributed programssatisfy equivalence properties.Those properties state that an attackercannot decide what scenario is beeing played.Strong secrecy, and privacy type properties, like anonymityand unlinkeability, can be modelled through this formalism.Moreover, protocols are executed simultaneouslyby an unbounded number of agents, for an unbounded numberof sessions,which leads to indecidability results.So, we have either to consider an arbitrary number of sessions,and search for semi-decision proceduresand decidable classes;or to establish decision procedures for a finite numberof sessions.When we started the work presented in this thesis,the existing equivalence checkers in the bounded modelwere highly limited. They could only handlea~very small number of sessions (sometimes no more than three).This thesis presents efficient decision proceduresfor bounded verification of equivalence properties.Our first step is to provide small attack results.First, for deterministic processes, there existsan attack if, and ony if, there is a well-typed attack,assuming that there is no confusion between variable types.Second, when there exists a flaw,the attacker needs at most three constants to find it.Then, our second step is to translatethe indistinguishability problem as a reachability problemin a planning system. We solve this second problemthrough planning graph algorithm and SAT encoding.In a final step, we present the implementation ofthe SAT-Equiv tool, which allows us to evaluate our approach.In particular, a benchmark with comparable tools provesthe efficiency of SAT-Equiv.

Cette thèse examine les conceptions de l'historicité de Michel Freitag et Cornelius Castoriadis. Les perspectives développées par ces deux auteurs seront d'abord rapprochées du concept d'historicisme, entendu comme reconnaissance de la relativité historique du monde social et comme volonté de poursuivre un projet d'objectivation. En cela, les deux auteurs à l'étude se situent dans le prolongement du problème ouvert par le concept d'historicisme. Ils ont voulu montrer les sources de l'historicité tout en maintenant un projet de vérité pour la philosophie et les sciences sociales. Pour prendre la pleine mesure de leur démarche, nous retracerons les questions principales des auteurs quant à cette conjonction historicité/vérité. Nous étudierons ainsi leurs conceptions du vivant et de l'animal, de manière à en saisir les spécificités tout comme ce que nous partageons avec ceux-ci. Nous nous attarderons ensuite sur la notion freitagienne du symbolique et les notions castoriadiennes d'imaginaire et de création, afin d'établir ce qui distingue le fait humain du fait animal pour chacun d'eux. Cela sera l'occasion de nous pencher sur l'origine du langage et la nature de la psyché afin d'établir ces différences. Les divergences notables entre l'ontologie générale des deux auteurs seront également analysées, tout comme leur très grande convergence sur les questions épistémologiques. Tous deux se revendiquent en effet d'une méthode compréhensive afin de saisir les caractéristiques d'une société particulière. Nous serons enfin en mesure d'examiner plus en détail les conditions sociohistoriques et ontologiques par lesquelles une société se reproduit et se crée de manière continue. Cette analyse nous mènera vers leurs oppositions proprement politiques : là où Freitag considère nécessaire et salvateur de maintenir un Tiers fondateur à distance du social, Castoriadis présente une conception non représentative et non étatique de la démocratie, proche du modèle athénien antique. Ressortira à chaque étape de cette vaste étude leur volonté de maintenir un projet de connaissance et de transformation de la société arrimé sur la conscience de l'historicité social-historique.

Žižek consacre une portion de sa pensée à la notion de révolution. Celle-ci concerne la façon de concevoir ce qu’est une révolution et le moyen de l’engager, l’un étant intimement lié à l’autre. Au cœur de cette réflexion, Žižek traite de l’interrogation nécessaire à tout projet révolutionnaire, à savoir comment faire pour provoquer une révolution. S’il soutient d’emblée que l’activité du sujet laquelle produit l’action révolutionnaire est constamment récupérée par la structure symbolique de son assujettissement, il formule néanmoins un moyen qui concerne la façon de penser l’activité du sujet laquelle permet à ce dernier de briser cette impasse. L’objectif de Žižek à cet égard est de réfléchir un moyen d’outrepasser la performativité du sujet face au symbolique, ce qu’il fait au travers du concept d’Acte qu’il qualifie de révolutionnaire. Ce mémoire vise à éclaircir la place que prend l’Acte comme medium d’instigation à la révolution, c’est-à-dire le moyen que Slavoj Žižek soutient comme étant ce qui permettrait aux révolutionnaires de court-circuiter l’impotence de leur activité lorsqu’elle se limite au symbolique. Dans un premier temps, afin de mettre en contraste la valeur d’un Acte, nous dresserons le portrait de l’action, soit de l’activité du sujet sous le langage. De la sorte, nous mettrons en évidence comment l’activité courante du sujet est considérée impotente en vue de tout projet qui a pour objet la provocation d’une révolution. Dans un second temps, nous présenterons ce que Žižek entend par "Acte". Nous verrons alors comment un Acte est ce qui outrepasse la récupération symbolique relative à l’action du sujet sous le langage en s’appuyant sur le Réel et comment alors en un tel dépassement se tient le potentiel de l’instigation d’une révolution. Nous conclurons en soutenant que bien qu’un Acte à la manière dont Žižek l’entend lui permette de soutenir le moyen d’instiguer une révolution, cela ne règle pas le cas de l’engagement du révolutionnaire envers son propre Acte, à savoir la relation que cultive le révolutionnaire avec son propre projet. / Žižek devotes a portion of his theory to the notion of revolution. It concerns the way to concieve what is a revolution and the medium to provoke it, one intimately bound to the other. At the heart of this reasonning, Žižek deals with a problem that is central to every revolutionnary project, that being understanding what it means to provoque a revolution. If he initially argues that the subject’s activity which produce revolutionnary actions is irrevocably recuperated by the symbolic structure which sustains them as subject, he nonehteless formulates a way to think differently the subject’s activity which would result in overcoming of the impass. With that, Žižek’s objectif is to think a way to surpass the subject’s symbolic performativity which he does through the concept of the Act that he qualifies as revolutionnary. This mémoire intend to unriddle the place that takes the Act as a medium of revolution, meaning the medium through which Žižek uphold as what could let revolutionnaries short-circut the impotence of their own symbolic activity. To begin with, in the spirit of contrasting the value of the Act, we will portray the action as the activity of the subject of language. This way, we will underscore how the social activity of the subject is considered impotent towards achieving any kind of revolutionnary project. Then, we will explore what Act means for Žižek. We will then see how an Act is what surpasses symbolic recuperation relative to the subject of language’s action by leaning on the Real and how is thus created the mean for a potential revolution. We will conclude by arguing that even though an Act as understood by Žižek lets him uphold a way to produce a revolution, this does not adress the way the revolutionnary subject is engaged towards his own Act, that being his relationship with his own project.

Au cours des années 1990, en Ontario, au moins quatorze individus furent accusés et déclarés responsables de la mort d’un enfant qui, au moment du décès, était seul en compagnie de l’inculpé. Plusieurs de ces condamnés furent acquittés à la suite de la découverte d’erreurs commises par le pathologiste médicolégal, tant durant l’autopsie qu’au cours de ses témoignages. Pourtant, il n’était pas le seul à en porter la responsabilité. Les erreurs judiciaires survenues lors de ces procès auraient-elles pu être atténuées par l’application de logique formelle au raisonnement judiciaire ? L’analyse qui suit comprend l’élucidation des erreurs, l’étude de théories de logique et du raisonnement, ainsi qu’un survol de la logique symbolique. L’aide-mémoire ainsi conçu représente un recours possible dans le but de rehausser le raisonnement judiciaire. La symbiose entre la logique et le raisonnement judiciaire s’avère possible, malgré l’écart entre les domaines de la science et du droit.

Dans le contexte actuel du développement des connaissances dans le domaine des sciences de l'orientation, certains chercheurs (Riverin-Simard, 1993, Vondracek, 2004) proposent aujourd'hui de concevoir le développement de carrière sous l'angle de perspectives théoriques qui favorisent la prise en compte de la relation personne-environnement (P/E). Ce mémoire propose d'explorer cette perspective en s'attardant à la contribution d'une formation de nature transactionnelle (relation P/E) sur les parcours d'insertion socioprofessionnelle. Afin d'investiguer le potentiel de cette perspective théorique, nous nous sommes attardés à l'approche interactionniste-stratégique (IS) enseignée à l'Université Laval dans le contexte de la formation des étudiants de la maîtrise en sciences de l'orientation. Bien évidemment, cette approche pragmatique est hautement compatible avec les caractéristiques du modèle théorique de l'approche transactionnelle sur lequel nous nous appuyons. Dans le cadre de ce mémoire de maîtrise, onze diplômés ayant suivi la formation en interactionnisme-stratégique et ayant entamé leur insertion socioprofessionnelle ont été rencontrés dans le cadre d'entrevues semi-dirigées afin qu'ils expriment la contribution de leurs apprentissages liés à cette formation, dans des situations concrètes d'insertion socioprofessionnelle. Leurs propos ont été enregistrés et analysés pour dégager les contextes d'insertion socioprofessionnelle où les notions IS ont pu être réinvesties ainsi que pour identifier les bénéfices qu'ils en ont retirés dans le cadre de leur insertion sur le marché du travail. Les résultats de cette étude exploratoire révèlent que la formation a un potentiel pour outiller les personnes à comprendre et agir sur des situations concernant les relations de travail (conflits, tensions), les rôles et conflits de rôles ainsi que pour appréhender la culture organisationnelle. Par contre, les habiletés d'analyse stratégique des situations complexes, enseignées dans le cadre de cette formation sont peu utilisées ou de manière superficielle dans ces contextes d'insertion socioprofessionnelle. Certains facteurs sont explorés dans la discussion pour expliquer ces résultats.

Ce mémoire porte sur l'analyse de l'univers symbolique du lait maternel en contexte maghrébin et s'appuie sur des recherches ethnologiques effectuées au début du XXe siècle et surtout depuis 1980 à aujourd'hui. Les tribus berbères sur lesquelles porte ce travail sont originaires du Maroc, les Ait Khebbach, et de l'Algérie, les Kabyles et les Chaouis. Les pouvoirs symboliques attribués au lait maternel engendrent des interdits et des rapports de protection. Les interdits sont induits par l'analogie entre le lait maternel et le sperme. Le lien symbolique établi entre la parenté par le lait, la radâ ', et la parenté par le sang entraîne des interdits matrimoniaux. La protection est basée sur l'investissement symbolique du lait maternel considéré comme un aliment primordial et civilisateur. Elle s'exprime particulièrement dans la tad'a, une alliance tribale fondée sur l'échange de lait maternel. Et comme le lait est un élément protecteur, on tente de le conserver par l'alimentation galactogène et les rituels de défense et de partage.

Thèse diffusée initialement dans le cadre d'un projet pilote des Presses de l'Université de Montréal/Centre d'édition numérique UdeM (1997-2008) avec l'autorisation de l'auteur. / Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal. / Un grand nombre des travaux réalisés par les ethnologues touchent à la dimension ethnique de la variation humaine. Cependant, les outils conceptuels qu'on emploie pour analyser ces phénomènes sont demeurés flous et sous-théorisés. Cette thèse a, par conséquent, un double but: celui de raffiner, sur la base d'une analyse critique, les outils conceptuels permettant de cerner le processus de construction de l'objet d'étude (l'identité ethnique), et celui de les appliquer à l'étude du processus de construction identitaire d'un groupe précis (les Gitans de la basse Andalousie). L'approche développée est non essentialiste, l'identité étant abordée ici comme un processus de construction sociale et historique. Ce n'est pas un contenu culturel ou des traditions qui déterminent les contours de cette identité mais, au contraire, le processus de construction de la frontière qui la définit. Cette thèse constitue une réflexion sur la frontière ethnique en tant que lieu d'expression de l'identité ethnique, et en tant que lieu d'étalage des produits symboliques que le groupe estime investis d'une signification différenciatrice. Le propos de cette étude était d'établir la nature des frontières de l'identité ethnique en explorant leur composition, leurs principes de construction, pour identifier les forces de leur transformation à l'œuvre historiquement et encore aujourd'hui. La méthodologie a emprunté deux voies parallèles : celle de la constitution des outils conceptuels et analytiques dans le cadre d'une théorie du social s'inspirant de celles de Pierre Bourdieu et d'Anthony Giddens et puis, celle de leur application dans l'étude de cas. Cette dernière comprenait les démarches suivantes : un examen critique de l'utilisation du concept d'identité ethnique dans la littérature concernant les groupes tsiganes en Europe en général et les Gitans d'Espagne en particulier; une recherche terrain de 17 mois (divisée en trois séjours) permettant la cueillette d'histoires de vie, d'une revue de presse, etc. Cette démarche permet de déceler une frontière ethnique discontinue, à intensité variable dans le temps et dans l'espace : un conglomérat de pratiques sociales et rituelles, non pas une barrière étanche, immuable et divorcée des pratiques quotidiennes et rituelles. Cette frontière s'établit autour de certaines pratiques sociales, celles qui sont perçues comme étant des enjeux pour l'identité, ce qui m'amène à proposer deux nouveaux concepts analytiques : celui de terrain d'investissement identitaire et celui d'afficheur identitaire. Ainsi, les Gitans de la basse Andalousie se constituent en tant que groupe à la fois en marge et en symbiose avec la société majoritaire, en se construisant des espaces propres au sein même des institutions de celle-ci. C'est ce qui leur a permis de rénover leurs stratégies identitaires malgré la transformation radicale du contexte socio-économique dans lequel elles évoluent. Les résultats de cette recherche ont une incidence tant au niveau théorique (en ce qui concerne l'identité ethnique et concepts afférents) et au niveau des politiques étatiques concernant les minorités ethniques qui, pour la plupart, se basent sur une conception de la frontière ethnique trop monolithique.

L’utilisation d’outils est un trait définitoire du genre Homo. Il est donc fondamental de mieux connaître les bases cognitives et cérébrales nous permettant d’utiliser des outils. Les modèles cognitivistes actuels expliquent l’utilisation d’outils à travers l’hypothèse de l’activation d’une mémoire gestuelle (i.e., engrammes gestuels ou visuo-kinétiques, ou connaissances sensorimotrices sur la manipulation ; voir Rothi, Ochipa, & Heilman, 1991 ; Buxbaum, 2001) ? Cette hypothèse ne permet toutefois pas de comprendre l’utilisation d’outils nouveaux. Une hypothèse alternative a été établie, suggérant que toute situation d’utilisation d’outils (familiers et nouveaux) requière un raisonnement technique (e.g., Osiurak & Badets, 2016). Ce type de raisonnement, qui impliquerait le lobe pariétal inférieur gauche, nous permettrait de formuler l’action mécanique et d’évaluer les propriétés physiques des outils et des objets. Dans le cadre de cette hypothèse, l’une des finalités de cette thèse était de mieux comprendre les troubles d’utilisation d’outils chez des patients cérébro-lésés. Le présent travail s’est également porté sur l’investigation de la cognition numérique. Par ce terme, nous ne faisons pas uniquement référence au calcul mental ou à l’arithmétique. Nous englobons également ce que Dehaene et Cohen (1995) ont nommé code analogique dans leur Modèle du Triple Code. Ce code stockerait les représentations des quantités numériques au sein des lobes pariétaux. Autrement dit, il contiendrait le sens du nombre (Dehaene, 1997) permettant d’associer une étiquette symbolique (e.g., chiffre arabe) à la quantité correspondante. Au quotidien, ce serait grâce à ces représentations que nous pourrions comparer ou estimer la numérosité des ensembles d’objets. L’objectif principal de cette thèse était de rapprocher, tant au niveau cognitif que cérébral, ces deux domaines d’intérêt que sont l’utilisation d’outils et la cognition numérique. En effet, nous avons remarqué que ces deux capacités nécessitaient toutes deux un processus commun d’estimation de la magnitude (i.e., magnitude des propriétés physiques et magnitude des quantités numériques). En outre, au niveau cérébral, elles nécessitent l’activation de régions communes dans le lobe pariétal. Pour penser ce lien, nous nous sommes appuyés sur la théorie de la magnitude (ATOM) formulée par Walsh (2003). Celui-ci postule que toutes les magnitudes, c’est-à-dire toutes les dimensions qui peuvent être décrites par des relations « plus que/moins que », soient traitées au sein d’un système commun et unique dans le lobe pariétal droit (Bueti & Walsh, 2009). Nous avons supposé que la magnitude des propriétés physiques pourrait être traitée dans ce système au même titre que les magnitudes discrètes (e.g., numérosité) et continues (e.g., temps, espace). Nos résultats ont mis en évidence un trouble de l’utilisation d’outils nouveaux chez les patients LBD, sans difficultés apparentes pour estimer les propriétés physiques. Les patients RBD étaient déficitaires dans toutes les conditions évaluant la cognition numérique, contredisant les prédictions issues du TCM. Ces patients étaient également en difficulté pour estimer la longueur mais pas le poids. Comme des associations entre estimation de la longueur et du poids, et entre estimation de la longueur et cognition numérique ont été observées dans les différents groupes, nous suggérons que le système de magnitude soit divisé en sous-systèmes. Fait étonnant, nous avons trouvé une association entre utilisation d’outils et calcul approximatif chez les patients LBD supposant une tentative de compensation de l’utilisation par le calcul. Finalement, il semble que l’utilisation d’outils et la cognition numérique reposent sur des mécanismes neurocognitifs distincts, puisque les différents types de magnitudes ne paraissent pas être traités au sein d’un système commun et unique. / Tool use is a defining feature of the genus Homo. It is therefore fundamental to better understand the cognitive and cerebral bases that allow us to use tools. The current cognitivist models explain tool use through the hypothesis of an activation of gestural memories (i.e., gestural or visuo-kinetic engrams, or sensorimotor knowledge of manipulation; see Rothi, Ochipa, & Heilman, 1991; Buxbaum, 2001). This theory is unable to explain the use of novel tools. An alternative hypothesis suggests that any situation of tool use (familiar and new) requires technical reasoning (e.g., Osiurak & Badets, 2016). This reasoning, involving the left inferior parietal lobe, would enable to formulate the mechanical action and to evaluate the physical properties of tools and objects. One of the aims of this thesis was to better understand the tool use disorders in brain-damaged patients, within the framework of the technical reasoning hypothesis. This work has also focused on the investigation of numerical cognition. By this term we refer to mental arithmetic and math, but also to analogical code (see the Triple Code Model, Dehaene & Cohen, 1995). It corresponds to the representation of numerical quantities, stored in the parietal lobes. In other words, this code would contain the sense of number (Dehaene, 1997) to associate a symbolic label (e.g., Arabic digits) with the corresponding quantity. In everyday life, this representation would be critical to compare or estimate the numerosity of object sets.The main objective of this thesis was to explore, at cognitive and cerebral levels, whether links exist between both fields of interest that are tool use and numerical cognition. Indeed, we noticed that both capacities need a common process of magnitude estimation (i.e., physical properties and numerical quantity). In addition, at the cerebral level, they require the activation of common regions in the parietal lobe. We relied on the Theory Of Magnitude (ATOM) formulated by Walsh (2003). It postulates that all magnitudes, namely the dimensions described by “more than/less than” relationships (e.g., Is this stick long enough to reach a given place?), are processed within a common and unique system, in the right parietal lobe (Bueti & Walsh, 2009). We assumed that the magnitude of physical properties could be processed in this system as well as the discrete (e.g., numbers) and continuous (e.g., time, space) magnitudes. Our results highlighted a disorder of novel tool-use in LBD patients, who nevertheless had no difficulty in estimating physical properties. The RBD patients were impaired in all conditions assessing the numerical cognition, refuting the predictions derived from TCM. They were also impaired in the estimation of the length but not of the weight. As associations between estimation of length and of weight, and between estimation of length and numerical cognition have been observed in the different groups, we suggest that the magnitude system be divided into subsystems. Surprisingly, we found an association between tool use and approximate calculation in LBD patients assuming an attempt to compensate tool use by calculation. Finally, it seems that tool use and numerical cognition rely on distinct neurocognitive mechanisms since the different types of magnitudes might not be processed within a common and unique system of magnitude