JavaScript est un langage de programmation maintenant très utilisé - y compris dans des domaines où la sécurité est importante. Il est donc important de permettre de vérifier la qualité des logiciels écrit en JavaScript. Cette thèse explore l'approche de la preuve formelle, visant à donner une preuve mathématique qu'un programme donné se comporte comme prévu. Pour construire cette preuve, nous utilisons un assistant de preuve tel que Coq - un programme de confiance permettant de vérifier nos preuves formelles. Pour pouvoir énoncer qu'un programme JavaScript se comporte correctement, nous avons tout d'abord besoin d'une sémantique du langage JavaScript. Cette thèse s'est donc inscrite dans le projet JSCert visant à produire une sémantique formelle pour le langage JavaScript. Devant la taille de la sémantique de JavaScript, il est important de savoir comment on peut lui faire confiance : une faute de frappe peut compromettre toute la sémantique. Pour pouvoir faire confiance à JSCert, nous nous sommes appuyés sur deux sources de confiance. D'une part, JSCert a été conçue pour être très similaire à la spécification officielle de JavaScript, le standard ECMAScript : ils utilisent les mêmes structures de donnée, et il est possible d'associer chaque règle de réduction dans JSCert à une ligne d'ECMAScript. D'autre part, nous avons défini et prouvé relativement à JSCert un interpréteur nommé JSRef. Nous avons aussi pu lancer JSRef sur les suites de test de JavaScript. La sémantique de JSCert n'est pas la première sémantique formelle pour le JavaScript, mais c'est la première à proposer deux manières distinctes pour relier la sémantique formelle au langage JavaScript : en ayant une sémantique très similaire à la spécification officielle, et en ayant testé cette sémantique pour la comparer aux autres interpréteurs. Plutôt que de prouver indépendamment que chaque programme JavaScript s'exécute comme prévu, nous analysons ses programmes par interprétation abstraite. Cela consiste à interpréter la sémantique d'un langage avec des domaines abstraits. Par exemple la valeur concrète 1 pourra être remplacée par la valeur abstraite +. L'interprétation abstraite se compose en deux étapes : d'abord une sémantique abstraite est construite et prouvée correcte vis à vis de sa sémantique concrète, puis des analyseurs sont construits selon cette sémantique abstraite. Nous ne nous intéresserons qu'à la première étape dans cette thèse. La sémantique de JSCert est immense - plus de huit cent règles de réduction. La construction d'une sémantique abstraite traditionnelle ne passent pas à l'échelle face à de telles tailles. Nous avons donc conçu une nouvelle manière de construire des sémantiques abstraites à partir de sémantiques concrètes. Notre méthode se base sur une analyse précise de la structure des règles de réduction et vise à minimiser l'effort de preuve. Nous avons appliqué cette méthode sur plusieurs langages. Dans le but d'appliquer notre approche sur JavaScript, nous avons construit un domaine basé sur la logique de séparation. Cette logique requiert de nombreuses adaptations pour pouvoir s'appliquer dans le cadre de l'interprétation abstraite. Cette thèse en étudie les interactions et propose une nouvelle approche pour les solutionner dans le cadre construit précédemment. Nos domaines, bien qu'assez simple par rapport au modèle mémoire de JavaScript, semblent permettre la preuve d'analyseurs déjà existant. Les contributions de cette thèse sont donc triples : une sémantique formelle de confiance pour le langage JavaScript, un formalisme générique pour construire des sémantiques abstraites, et un domaine non trivial pour ce formalisme. / JavaScript is a trending programming language. It is not used in applications in which security may be an important issue. It thus becomes important to be able to control the quality of softwares written in JavaScript. This thesis explores a formal proof approach, which aims at giving a mathematical proof that a given program behaves as expected. To build this proof, we use proof assistants such as Coq—a trusted program enabling to check formal proofs. To state that a JavaScript program is behaving as expected, we first need a semantics of the JavaScript language. This thesis is thus part of the JSCert project, whose aim it to prove a formal semantics for JavaScript. Because of the size of JavaScript's semantics, it is crucial to know how it can be trusted: a typing mistake could compromise the whole semantics. To trust JSCert, we based ourselves on two trust sources. On one hand, JSCert has been designed to be the most similar it can be from the official JavaScript specification, the ECMAScript standard: they use the same data structures, and it is possible to relate each derivation rule in JSCert to a line of ECMAScript. On the other hand, we defined and proved correct with respect to JSCert an interpreter named JSRef. We have been able to run JSRef on JavaScript test suites. The JSCert semantics is not the first formal semantics of JavaScript, but it is the first to propose two distinct ways to relate the formal semantics to the JavaScript language: by having a semantics close to the official specification, and by testing this semantics and comparing it to other interpreters. Instead of independently proving that each JavaScript program behaves as expected, we chose to analyse programs using abstract interpretation. It consists of interpreting the semantics of a programming language with abstract domains. For instance, the concrete value 1 can be replaced by the abstract value +. Abstract interpretation is split into two steps : first, an abstract semantics is built and proven correct with respect to its concrete semantics, then, analysers are built from this abstract semantics. We only focus on the first step in this thesis. The JSCert semantics is huge - more than height hundred derivation rules. Building an abstract semantics using traditional techniques does not scale towards such sizes. We thus designed a new way to build abstract semantics from concrete semantics. Our approach is based on a careful analysis on the structure of derivation rules. It aims at minimising the proof effort needed to build an abstract semantics. We applied our method on several languages. With the goal of applying our approach to JavaScript, we built a domain based on separation logic. This logic require several adaptations to be able to apply in the context of abstract interpretation. This thesis precisely studies these interactions and introduces a new approach to solve them in our abstract interpretation framework. Our domains, although very simple compared to the memory model of JavaScript, seems to enable the proof of already existing analysers. This thesis has thus three main contributions : a trusted formal semantics for the JavaScript, a generic framework to build abstract semantics, and a non-trivial domain for this formalism.

Les failles sont des zones de rupture de la roche qui affectent le comportement mécanique et fluide des réservoirs. De nombreuses incertitudes existent sur la géométrie et la topologie des réseaux de failles dues à la résolution et la qualité des données, mais aussi aux lacunes d'informations. Des approches stochastiques ont été utilisées dans la littérature pour gérer les incertitudes structurales. Ces méthodes génèrent un ensemble de modèles possibles de failles conditionné par les données disponibles. Dans cette thèse, nous explorons deux principales stratégies de conditionnement de la modélisation stochastique de réseaux de failles. La première stratégie élaborée permet de prendre en compte des observations d'absences de failles sur des données, par exemple, des zones où les réflecteurs sismiques sont continus. Dans ce but, le réservoir est divisé en deux sous-volumes délimités par une enveloppe surfacique 3D : un volume non-faillé et un volume potentiellement-faillé. Les surfaces de failles sont ensuite simulées et optimisées de manière à être entièrement positionnées dans la zone identifiée comme potentiellement faillée. La seconde stratégie de conditionnement présentée dans cette thèse gère les incertitudes relatives à l'interprétation de la segmentation des failles. La méthode génère un ensemble de modèles de segments de failles en-échelon à partir d'une interprétation continue à plus grande échelle d'une faille segmentée. La méthode utilise les variations d'orientations de la faille segmentée pour identifier la position des différents segments la composant. L'impact des différentes configurations de segmentation sur les simulations d'écoulements est étudié / Faults are discontinuities in rock volumes that affect mechanical properties and flow paths of hydrocarbon reservoirs. However, subsurface modeling remains limited by the incompleteness and resolution of available data, so that uncertainties remain on the geometry and the connectivity of fault networks. To assess fault network uncertainties, several stochastic approaches have been introduced in the literature. These methods generate a set of possible fault models conditioned by reservoir data. In this thesis, we investigate two main conditioning strategies of stochastic fault modeling methods. The first one takes into account the observations of the fault absence, for instance, as indicated by seismic reflector continuity. To do this, the reservoir volume is divided into two sub-volumes delimited by a 3D envelope surface: (1) a volume where no faults occur, and (2) a potentially-faulted volume. Then, faults are simulated and optimized in such a way as to be entirely confined to the potentially-faulted volume. The second presented strategy deals with the uncertainties related to the seismic interpretation of fault segmentation. It generates a set of fine-scale segmented faults from a larger-scale and continuous interpretation of the fault. The method uses the orientation variations of the continuous fault to subdivide it into several possible fault segments. The effects of the different segmentation configurations on flow simulations are studied

Dans cette thèse, nous cherchons à penser les enjeux philosophiques de l’application de méthodes herméneutiques en histoire de la philosophie politique. À partir d’une étude comparative des interprétations de l’œuvre de Nicolas Machiavel offertes par Leo Strauss, Quentin Skinner et Claude Lefort, nous interrogeons le rapport que l’interprète institue avec le texte qu’il étudie. Nous montrons qu’il y a dans les trois cas un écart entre l’exposition théorique des principes herméneutiques et l’application effective de ces derniers. Nous soutenons que les divergences fondamentales entre les trois lectures des écrits machiavéliens ne trouvent pas leur fondement dans la différence des méthodes employées, mais proviennent en dernier lieu de la compréhension particulière qu’ils ont du rôle et du statut de la pensée de Machiavel. Autrement dit, nous cherchons à montrer que l’intérêt pour la signification de l’œuvre machiavélienne dépasse la simple analyse des écrits d’un auteur du passé; les trois interprètes entretiennent un rapport singulier à la pensée du secrétaire florentin. En ce sens, l’étude des herméneutiques de Strauss, Skinner et Lefort appliquées à Machiavel est indissociable d’une interrogation sur l’articulation entre interprétation et politique.

Cette thèse propose de définir une génération d’artistes dont la spécificité consiste à collecter, associer et rediffuser des images existantes, sans en transformer le contenu iconique. Pour tenter de cerner les caractéristiques de cette pratique, des entretiens ont été menés avec des artistes français contemporains : Eric Baudelaire, Ludovic Burel, Hervé Coqueret, documentation céline duval, Pierre Leguillon, Mathieu Pernot, Régis Perray et Eric Watier. L’analyse des dispositifs plastiques qu’ils mettent en œuvre fait apparaître deux aspects susceptibles d’identifier la spécificité de leur travail : leur manière d’associer les images entre elles suscite de nouvelles interprétations entraînant leur relecture ; et leur pratique s’inscrit dans une phase transitoire entre l’ère de la reproductibilité technique des images et celle des technologies du numérique. A travers une recherche scientifique pluridisciplinaire, il sera donc question d’étudier leurs processus de création depuis le choix des images jusqu’à la diffusion de leurs projets (I), d’analyser la polysémie des images et les possibilités d’en relire les signes (II) et enfin de comprendre comment s’agence leur position artistique entre deux époques techniquement marquées concernant les images (III). Afin de les démarquer des autres générations réemployant des images, la thèse propose une nouvelle dénomination : les Relecteurs d’images. / This thesis proposes to define a generation of artists who are collecting, associating and redistributing pictures without changing or transforming the iconic contents. In order to elaborate their characteristics, several french contemporary artists were interviewed: Eric Baudelaire, Ludovic Burel, Hervé Coqueret, documentation céline duval, Pierre Leguillon, Mathieu Pernot, Régis Perray and Eric Watier. The analysis of the devices implemented by the artists shows two aspects that could identify the specificity of their work: their way of associating the pictures with each other offers new possibilities of interpretation and leads to a second reading of the pictures; and their practice is taking place during the transition between the eras of image reproduction techniques and numerical techniques. Within the scope of a multi-field scientific research, it will be necessary to study the creation processes from the choice of the representation till the distribution of the projects (I), to analyse the polysemy of the images and the possibility of rereading their signs (II), and, finally, to understand how the artistic position is located between two, with respect to pictures, technically distinguished epoches (III). To differentiate this generation of artists from others reusing images, the thesis suggests a new name: the “Rereaders of pictures”.

Cette recherche a pour but, premièrement, de reconnaître les traits distinctifs de la pédagogie dans l’enseignement thaïlandais, dans ses relations à la culture. Notre analyse s’appuie sur l’enseignement de la langue thaïe et de la langue française, plus particulièrement sur le développement des compétences linguistiques nécessaires à la compréhension textuelle dans ces deux langues. Pour appuyer cette étude, nous nous référons au Cadre Européen Commun de Référence pour les langues. Nous nous intéressons également aux compétences métacognitives, et plus précisément métalinguistiques, dont le rôle s’avère important lors de la reformulation de la compréhension. Deuxièmement, cette enquête tend à comprendre l’activité de lecture des apprenants de FLE. Nous mettons l’accent sur le processus d’interprétation au cours duquel l’insuffisance ou l’incohérencedes compétences linguistiques peuvent causer l’incompréhension. Troisièmement, en plus des compétences linguistiques, nous pensons que la subjectivité personnelle peut aussi influencer les opérations d’interprétation du texte. Les arts du texte, selon laconception de F. Rastier, nous conduit à observer les différentes opérations d’interprétation mises en oeuvre par chaque apprenant afin de comprendre un même texte. Dans cette enquête, nous insistons sur l’emploi de l’anaphore, plus particulièrement l’expression nominale on, dont la valeur référentielle est particulièrement difficile à identifier / The primary objective of our research is to identify and bring to the fore, in Thailand’s educational system, the distinctive features of the sciences or art of teaching with reference to culture. Our analysis is based on the teaching of both Thai and French languages, and more especially on linguistic competence the learner needs in order to understand written texts in both languages. We copiously referred to The Common European Framework of Reference for Languages to support thisanalysis. In the same vain, we made reference to meta-cognitive competences, and especially metalinguistic ones whose role is of paramount importance in the reconstruction of understanding/comprehension. On the other hand, this research aims at understanding the reading activities of Thai learners of French language. We lay emphasis on the interpretation process during which the lack or incoherency of linguistic competence could hinder understanding. Finally, beside linguistic competence, we believe individual subjectivity can also influence the operations involved in interpreting a text. The arts of text (understanding), according to F. Rastier, allow us to critically observe the different interpretation or reconstruction operations used by each learner in his bid to understand a text. In this respect we explore the use of anaphor, and particularly the nominal French expression ‘on’ which referential value is often very difficult to grasp

Le piano de Xenakis, comme tous les langages instrumentaux du compositeur, reste un objet assez singulier dans la littérature de l’instrument. Encore aujourd’hui rarement abordé par les pianistes, il semble d’une difficulté vertigineuse, et les voies qui mènent à sa réalisation restent dissimulées. L’originalité du langage musical du compositeur génère une technique extrêmement détachée de la tradition pianistique, et un pianiste manque souvent de savoir-faire et d’outils pour parvenir à l’exécution. Dans cette recherche nous essaierons d’aborder ce lien entre les principaux concepts xénakiens (musique stochastique, musique symbolique, mouvement brownien et pans ondulatoires, arborescences, cribles) et son langage pianistique, afin de mieux identifier cette écriture instrumentale et envisager des chemins pouvant favoriser l’interprétation de cette musique. Nous étudions la totalité des œuvres avec piano, puis nous explorons chacun des grands concepts du compositeur, pour établir ensuite leur connexion avec le langage pianistique dans quatre œuvres majeures pour le piano : Herma, Synaphaï, Evryali, Mists. Pour chacune de ces œuvres nous effectuons une analyse, puis proposons une approche pianistique visant le travail, l’exécution et l’interprétation. / Xenakis’ piano, like all the composers’ instrumental languages, remains a rather peculiar issue in the literature of the instrument, still rarely approached by pianists, not only because of its obvious difficulty, but mostly because of the great number of question raised by it, questions related to its feasibility and execution. The originality of the composer’s musical language generates a technic extremely detached from piano tradition, and a pianist often lacks the savoir-faire and the tools to reach a convincing execution of these works. In this research we try to approach the link between the principal xenakian concepts (stochastic music, symbolic music, Brownian movement and wave-like sides, arborescences, sieves) and the pianistic language related to it, in order to identify Xebakis’ writing for the instrument and consider the ways that the performance of this music can take place. We study briefly the whole output of Xenakis’ piano works (solo, concerto, chamber music, piano in the orchestra), then we explore each of the composer’s main concepts, in order to establish their connection to the pianistic language in four major works for piano : Herma, Synaphaï, Evryali, Mists. For each one of these works, we first perform an analysis, then we propose a pianistic approach aiming at the preparation and the performance.

Notre thèse se situe dans le champ de recherche des études de la réception des médias depuis une approche sémio-pragmatique qui vise en particulier le rapport des spectateurs avec le texte dans le cadre des pratiques discursives dans la culture de fans. L’objectif général de cette thèse est de comprendre comment se développent les pratiques discursives réalisées à partir de la réception de textes médiatiques. Le sujet général est la réception des médias, mais nous avons situé notre démarche dans le champ de la culture des fans, où les discussions du texte et les remaniements et réécritures sont des pratiques qui se réalisent couramment. L’intérêt est alors de parler de la réception dans le cadre de la pratique culturelle qui lui donne sens. Le groupe de fans que nous avons abordé pour notre travail est celui formé autour de la série télévisée Twin Peaks. Dans ce travail, nous cherchons à comprendre cette énorme diversité de productions de fans (discussions, créations, manipulation de textes) témoignant certainement de la réception de ces spectateurs, mais dont il faut saisir la stratégie face au faire énonciatif. Nous nous intéressons alors au rapport créé avec le texte. Notre objectif est d’essayer de comprendre la dynamique qui gouverne ces échanges et ces productions autour d’un texte médiatique. Il s’agit de montrer la logique de la réception et de l’appropriation des textes dans la culture des fans, de façon à comprendre comment ceux-ci et leurs communautés agissent en tant que spectateurs stratégiques. / This thesis, inscribed within the research field of media reception, follows a semio-pragmatic approach to study the dynamics between spectators and media as they appear within the context of discursive practices developed by fan culture. Its main goal is to understand how these discursive practices develop from the reception of media texts. Although its general field is media reception, the work focuses on fan culture because in it one can find well-established practices of text discussions, manipulation of content, and rewriting. Our interest is to study media reception in the cultural frame that provides it with meaning. The thesis follows the activities of the fandom of the television series Twin Peaks. In our work, we try to understand the enormous diversity of fan practices (forum discussions, fan-made creations, manipulations) which show the complexity of media reception, aiming to recognize the form which spectator strategies take when facing media strategies. Our greatest interest is to give sense to the complexity of the relations which spectators establish with media texts, thus aiming to explore the dynamics which govern the discussions and practices surrounding the media text. We will attempt to show the logics of media reception and appropriation within fan culture in order to understand how the fans and their communities act as strategic spectators.

Ce travail avait pour objectif d'étudier l'intérêt et les limites de l'analyse de deux matrices alternatives que sont la bile et l'humeur vitrée (HV), en toxicologie médicolégale. Pour chacune des deux matrices, une revue de la littérature visait à investiguer les connaissances utiles à leur application en toxicologie médicolégale. Une place importante de ces revues est réservée à l'anatomie et la physiologie de l'HV et du système biliaire ainsi qu'aux mécanismes de distribution des xénobiotiques dans ces matrices. La partie expérimentale décrit trois études: deux menées sur populations autopsiques et une associant expérimentations animales et études de populations autopsiques. Les deux premières ont permis de proposer des outils statistiques d'interprétation des concentrations de méprobamate mesurées dans ces matrices. Ils peuvent être utilisés dans diverses situations à la place ou en complément de l'interprétation des concentrations sanguines: cadavre exsangue, putréfaction avancée du corps, redistribution post mortem des xénobiotiques… La troisième étude concernait six molécules (diazépam, citalopram, cyamémazine, morphine, caféine et méprobamate). Les molécules détectées dans le sang l'étaient systématiquement dans l'HV et la bile aussi bien dans les prélèvements des populations autopsiques que ceux issus des expérimentations animales. Les concentrations vitréennes chez l'animal et chez l'homme étaient systématiquement corrélées aux concentrations sanguines, exceptées celles de cyamémazine et de citalopram chez l'homme. Pour la bile, une corrélation significative était observée pour le méprobamate et la caféine chez l'homme et l'animal. Il ressort de ces résultats, que l'analyse de l'HV et de la bile permettent de disposer d'informations relatives à la nature des molécules absorbées et à leur rôle dans la survenue du décès / The present study sought to assess the interest and limitations of analyzing two alternative matrices, bile and vitreous humor (VH), in forensic toxicology. For each matrix, a literature review established the state of knowledge relating to their forensic application. The review placed special focus on the anatomy and physiology of VH and the biliary system and the mechanisms of xenobiotic distribution within the specific matrix. The experimental sections describe three studies: two performed on autopsy populations, and one associating autopsy populations to an animal model. The first two studies resulted in statistical tools for interpreting meprobamate concentrations in these matrices, which can be used as alternatives or complements to blood concentrations in various situations: exsanguination, advanced putrefaction, postmortem xenobiotic redistribution, etc. The third study focused on 6 molecules: diazepam, citalopram, cyamemazine, morphine, caffeine and meprobamate. Molecules detected in blood were also systematically detected in VH and bile samples from both the autopsy and animal populations. Animal VH and blood levels showed systematic correlation. In autopsy samples, cyamemazine and citalopram showed no such correlation. In bile, significant correlations with blood concentrations were found for meprobamate and caffeine in both the autopsy and animal populations. This study confirmed the interest of postmortem analysis of bile and VH. Results show that analyzing bile and VH sheds light on drugs intake and on their implication in cause of death

Doctorat en philosophie et lettres / TH-000230 :Tome 1 - études / info:eu-repo/semantics/nonPublished

Cette thèse est une contribution à la spécification et à la vérification formelles des allocateurs de mémoire dynamiques séquentiels (SDMA, en abrégé), qui sont des composants clés des systèmes d'exploitation ou de certaines bibliothèques logiciel. Les SDMA gèrent la partie tas de la mémoire des processus. Leurs implémentations utilisent à la fois des structures de données complexes et des opérations de bas niveau. Cette thèse se concentre sur les SDMA qui utilisent des structures de données de type liste pour gérer les blocs du tas disponibles pour l'allocation (SDMA à liste).La première partie de la thèse montre comment obtenir des spécifications formelles de SDMA à liste en utilisant une approche basée sur le raffinement. La thèse définit une hiérarchie de modèles classés par la relation de raffinement qui capture une grande variété de techniques et de politiques employées par le implémentations réelles de SDMA. Cette hiérarchie forme une théorie algorithmique pour les SDMA à liste et pourrait être étendue avec d'autres politiques. Les spécifications formelles sont écrites en Event-B et les raffinements ont été prouvés en utilisant la plateforme Rodin. La thèse étudie diverses applications des spécifications formelles obtenues: le test basé sur des modèles, la génération de code et la vérification.La deuxième partie de la thèse définit une technique de vérification basée sur l'interprétation abstraite. Cette technique peut inférer des invariants précis des implémentations existantes de SDMA. Pour cela, la thèse définit un domaine abstrait dont les valeurs representent des ensembles d'états du SDMA. Le domaine abstrait est basé sur un fragment de la logique de séparation, appelé SLMA. Ce fragment capture les propriétés liées à la forme et au contenu des structures de données utilisées par le SDMA pour gérer le tas. Le domaine abstrait est défini comme un produit spécifique d'un domaine abstrait pour graphes du tas avec un domaine abstrait pour des sequences finies d'adresses mémoire. Pour obtenir des valueurs abstraites compactes, la thèse propose une organisation hiérarchique des valeurs abstraites: un premier niveau abstrait la liste de tous les blocs mémoire, alors qu'un second niveau ne sélectionne que les blocs disponibles pour l’allocation. La thèse définit les transformateurs des valeurs abstraites qui capturent la sémantique des instructions utilisées dans les implémentations des SDMA. Un prototype d'implémentation de ce domaine abstrait a été utilisé pour analyser des implémentations simples de SDMA. / The first part of the thesis demonstrates how to obtain formal specifications of free-list SDMA using a refinement-based approach. The thesis defines a hierarchy of models ranked by the refinement relation that capture a large variety of techniques and policies employed by real-work SDMA. This hierarchy forms an algorithm theory for the free-list SDMA and could be extended with other policies. The formal specifications are written in Event-B and the refinements have been proved using the Rodin platform. The thesis investigates applications of the formal specifications obtained, such as model-based testing, code generation and verification.The second part of the thesis defines a technique for inferring precise invariants of existing implementations of SDMA based abstract interpretation. For this, the thesis defines an abstract domain representing sets of states of the SDMA. The abstract domain is based on a fragment of Separation Logic, called SLMA. This fragment captures properties related with the shape and the content of data structures used by the SDMA to manage the heap. The abstract domain is defined as a specific product of an abstract domain for heap shapes with an abstract domain for finite arrays of locations. To obtain compact elements of this abstract domain, the thesis proposes an hierarchical organisation of the abstract values: a first level abstracts the list of all chunks while a second level selects only the chunks available for allocation. The thesis defines transformers of the abstract values that soundly capture the semantics of statements used in SDMA implementations. A prototype implementation of this abstract domain has been used to analyse simple implementations of SDMA