Le sujet de cette thèse est le développement de méthodes pour l'analyse automatique des programmes informatiques. Une des applications majeures est la conception d'outils pour découvrir les erreurs de programmations avant qu'elles ne se produisent, ce qui est crucial à l'heure où des tâches critiques mais complexes sont confiées à des ordinateurs. Nous nous plaçons dans le cadre de l'interprétation abstraite, qui est une théorie de l'approximation sûre des sémantiques de programmes, et nous nous intéressons en particulier aux domaines abstraits numériques spécialisés dans la découverte automatique des propriétés des variables numérique d'un programme.<br />Dans cette thèse, nous introduisons plusieurs nouveaux domaines numériques abstraits et en particulier le domaine des zones (permettant de découvrir des invariants de la forme X-Y≤c, des zones de congruence (X≡Y+c [b]) et des octogones (±X ±Y≤c). Ces domaines sont basés sur les concepts existants de graphe de potentiel, de matrice de différences bornées et sur l'algorithmique des plus courts chemins. Ils sont intermédiaires, en terme de précision et de coût, entre les domaines non relationnels (tel celui des intervalles), très peu précis, et les domaines relationnels classiques (tel celui des polyèdres), très coûteux. Nous les nommons " faiblement relationnels ". Nous présentons également des méthodes permettant d'appliquer les domaines relationnels à l'analyse de nombres à virgule flottante, jusqu'à présent uniquement réalisable par des domaines non relationnels donc peu précis. Enfin, nous présentons des méthodes génériques dites de " linéarisation " et de " propagation de constantes symboliques " permettant d'améliorer la précision de tout domaine numérique, pour un surcoût réduit.<br />Les méthodes introduites dans cette thèse ont été intégrées à Astrée, un analyseur spécialisé dans la vérification de logiciels embarqués critiques et se sont révélées indispensables pour prouver l'absence d'erreurs à l'exécution de logiciels de commande de vol électrique. Ces résultats expérimentaux viennent justifier l'intérêt de nos méthodes pour des cadre d'applications réelles.

Reproduction de : Thèse de doctorat : Informatique : Lille 1 : 2004. / N° d'ordre (Lille 1) : 3467. Résumé en français et en anglais. Titre provenant de la page de titre du document numérisé. Bibliogr. 9 p.

Le sujet de cette thèse est le développement de méthodes pour la découverte automatique des propriétés des variables numériques d'un programme. Nous nous plaçons dans le cadre de l'interprétation abstraite et introduisons plusieurs nouveaux domaines numériques, dont celui des octogones, de coût et de précision intermédiaires entre les domaines non relationnels (peu précis) et relationnels (coûteux) existants. Nous présentons leur adaptation à l'analyse des nombres à virgule flottante, jusqu'à présent limitée aux domaines non relationnels. Enfin, nous présentons les méthodes génériques de linéarisation et de propagation symbolique améliorant leur précision pour un surcoût réduit. Les méthodes introduites dans cette thèse ont été intégr! ées à l'analyseur Astrée et appliquées à la preuve d'absence d'erreurs dans le logiciel embarqué critique de commande de vol des avions Airbus A340, justifiant ainsi l'intérêt de nos méthodes pour des cadres d'applications réelles.

La classification des groupes simples finies achevée en 2004 par Aschbacher et Smith au terme de décennies de travaux par des centaines de mathématiciens livre 18 familles infinies et 26 groupes appelés sporadiques. Ces derniers sont dotés de propriétés singulières. Dans ma thèse de doctorat, nous étudions le groupe sporadique de O'Nan -- usuellement dénoté O'N -- d'un point de vue géométrique, dans la lignée des travaux des Professeurs Buekenhout, Dehon et Leemans.<p><p>Nous abordons essentiellement quatre facettes de la géométrie de O'N. Tout d'abord, nous produisons la classification complète des géométries Buekenhout--Cara--Dehon--Leemans (BCDL) de O'N, une tâche commencée par Leemans en 2010. Les géomé-tries BCDL sont caractérisées par des axiomes inspirés de la Théorie des Immeubles de Jacques Tits. La majorité des groupes simples finis sont caractérisés par un immeuble et un diagramme. Parmi les exceptions se trouvent les groupes sporadiques. Une géométrie BCDL est plus générale qu'un immeuble, mais s'en rapproche.<p><p>Ensuite, nous étudions une géométrie pour le groupe d'automorphismes de O'N construite à partir de paires d'involutions commutantes. Les involutions jouent un rôle majeur dans la théorie des groupes simples finis. Ces travaux sont inspirés de la construction d'une tour de géométries pour les groupes de Fischer construite à partir de paires d'involutions commutantes due à Buekenhout.<p><p>Nous poursuivons en étudiant les polytopes abstraits réguliers sur lesquels O'N agit. Nous produisons la classification des polytopes de rang maximum, à savoir 4.<p><p>Enfin, nous étudions O'N sous le spectre des cartes régulières. Tout polyèdre abstrait régulier est une carte régulière, mais la réciproque n'est pas vraie. Nous donnons un algorithme permettant d'énumérer par type les cartes régulières pour un groupe fini donné. Ceci nous permet de borner le nombre de polyèdres abstraits réguliers sur lesquels O'N agit.<p><p>Nous produisons également les treillis de sous-groupes de O'N et de son groupe d'automorphismes. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Un des grands enjeux actuels dans le domaine de la synthèse sonore consiste à proposer des stratégies de contrôle intuitif accessible à un grand nombre d'utilisateurs. Parmi les attributs fondamentaux du son, ceux qui sont liés au mouvement restent encore largement inexplorés et, de fait, difficilement contrôlables. Cette thèse s'intéresse à la perception des caractéristiques des sons monophoniques qui varient au cours du temps et qui sont à l'origine de la notion perceptive de ''mouvement évoqué'', ainsi qu'à la mise au point d'une stratégie de contrôle intuitif. Pour cela, nous avons mis au point une série d'expériences basées sur des protocoles de catégorisation et d'évaluation sonore par le biais de dessins via une interface graphique paramétrée. Afin de favoriser l'écoute sur les attributs intrinsèques du son, nous avons privilégié l'utilisation de sons dits ''abstraits" pour lesquels la source physique n'est pas facilement identifiable. Les résultats de ces expériences nous ont permis de définir un ensemble de dimensions perceptives importantes pour la caractérisation du mouvement évoqué, telles que la forme de la trajectoire, l'orientation ou bien la taille. Ces dimensions ont été par la suite validées grâce à un protocole expérimental exploitant la synthèse sonore. Le travail réalisé ouvre de nombreuses perspectives, notamment dans les domaines de la réalité virtuelle, du ''design sonore'' et de la musique. La méthodologie proposée vise à être suffisamment générale pour être transposable à l'étude d'autres attributs perceptifs liés au ressenti (émotions, qualité ...). / An important issue within sound synthesis, is to propose intuitive control strategies that are accessible to most potential users. Among fundamental sound attributes, the ones linked to motion are almost unexplored and thus cannot be easily controlled. This Ph.D. concerns the perception of time varying characteristics of monophonic sounds, which leads to the notion of motion evoked by sounds and the conception of intuitive control strategies for such motions. To address those questions, we developed several experiments based on categorization tasks and evaluations through drawings using a parameterized graphical interface. In order to help listeners focus on intrinsic sound attributes, we mainly used so-called ''abstract'' sounds for which the physical sound source is not easily recognizable. The results of those experiments enabled us to identify attributes that characterize evoked motion from a perceptual point of view, such as shape, direction and size of the trajectory. Those dimensions were further validated in an experimental protocol using sound synthesis. This work opens many perspectives, in particular within virtual reality, sound design and musical domains. The proposed methodology aimed at being sufficiently generic to be transposed to other perceptual attributes such as emotions and quality.

Notre thèse a pour thème l'émergence de l'objet social " violence domestique " et sa nomination dans le discours du Conseil de l'Europe en français. L'analyse est menée sur un corpus de textes officiels et préparatoires rédigés entre 1985, date de la première recommandation sur la violence au sein de la famille, et 2008, année d'achèvement de la Campagne pour combattre la violence à l'égard des femmes, y compris la violence domestique. La nomination est appréhendée comme une pratique à la fois reflétant la réalité sociale et contribuant à la construire. La valeur sociale et institutionnelle de violence domestique est analysée à partir d'une comparaison avec l'usage et la distribution des fréquences d'autres désignations très fréquentes en corpus [violence au sein de la famille et violence conjugale]. Désignations et définitions construisent discursivement la " violence domestique " en tenant compte des contraintes d'une organisation universaliste, dont l'objectif est de diffuser le respect des droits humains aussi bien dans la sphère publique que dans la sphère privée en dépassant les particularismes culturels ou géographiques de ses États membres. Le discours du Conseil de l'Europe est aussi traversé par la mémoire du discours militant féministe qui a permis de dévoiler la violence privée comme étant un des effets de la domination masculine sur les femmes. Au carrefour entre sémantique lexicale et analyse du discours, l'émergence de violence domestique en 1998 et sa diffusion comme dénomination officielle entre 2002 et 2008 sont observées comme relevant de son caractère vague et inclusif mais aussi des effets d'interférence de l'anglais sur le français dans le cadre du discours des institutions internationales.

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique

Le platonisme mathématique, la thèse selon laquelle les mathématiques portent sur des objets abstraits existant de manière indépendante à notre esprit et notre langage, est un des sujets les plus débattues dans la philosophie des mathématiques. L’image des mathématiques qui s’en dégage est souvent perçue comme se heurtant à des problèmes épistémologiques considérables : si il est vrai que les mathématiques sont une science qui porte sur des objets en dehors de l’espace et du temps, comment nous, des êtres situés spatio-temporellement, pouvons avoir une quelconque connaissance mathématique ? En conséquence, la défense du platonisme et le débat sur l’ontologie des mathématiques se sont largement concentrées sur cette dimension épistémologique. Dans ce travail de thèse, nous essaierons de réitérer le rôle de la métaphysique et de la pratique des mathématiques dans le débat sur l’ontologie des objets mathématiques. Notre objectif principal est plus particulièrement le développement et l’application d’un programme métaphysique général, capable de rendre compte des aspects ontologiques des mathématiques qui sont propres à une interprétation platoniste des mathématiques. Pour ce faire, notre stratégie consiste à insister tout d’abord sur le besoin de clarification des thèses platonistes concernant la nature abstraite des objets mathématiques et l’indépendance de ces objets et à essayer d’étendre la portée du platonisme au-delà des concepts et théories mathématiques habituelles. / Mathematical platonism is the idea according to which mathematics is about a domain of abstract objects, existing independently of our though and language. It is one of the central subjects in philosophy of mathematics, and is often considered to face important epistemological problems. If, as the platonist thinks, mathematics really are a science of objects outside of space and time, then how is mathematical knowledge even possible? As a consequence of the epistemological problem, the debate has focused mainly around the epistemological dimension of platonism. In this study however, we will try to move away from epistemology and restate the role of metaphysics and mathematical practice in the ontological debate on mathematical objects. Our main objective will be to develop and apply a general metaphysical program in order to explain the ontological aspects of a platonist interpretation of mathematics. In order to do this, it will be necessary to clarify the abstract nature of mathematical objects and the ontological independence of these entities, and to extend the scope of platonism beyond the usual concepts and mathematical theories.

Les espaces d'ordres abstraits sont introduits par M. Marshall dans les années 70, dans la perspective d'offrir un cadre abstrait à l'étude des formes quadratiques. Vers le début des années 90, les travaux de M. Dickmann, L. de Lima et de F. Miraglia, ont donné naissance à la version duale des groupes spéciaux. Le premier thème que nous traiterons est la caractérisation des points d'un espace d'ordres du corps de fonctions d'une variété réelle, nous reprendrons un résultat de Brumfiel affirmant l'existence d'une correspondance entre ces ordres et des ultrafiltres de semi-algébriques. Nous appliquerons ceci au corps R(x,y). Suivra la caractérisation des ordres de ce corps à travers la notion de demi-branche de Bézout. Le second thème traite des principes locaux-globaux généralisés (ou Conjecture pp). Le premier résultat de la thèse porte sur la séparation des constructibles et sur la principalité des basiques. Nous montrerons que le langage des groupes spéciaux nous offre une vision claire du fait que ces principes découlent trivialement du principe de l'isotropie étendu. Le second résultat traite des contre-exemples à la conjecture dans le cas de la conique rationnelle donnée par l'équation x2+y2=3. Le dernier résultat (le plus important), aborde la conjecture pp dans le cadre du corps R(x,y). Nous nous intéresserons à des familles de polynômes vérifiant certaines conditions géométriques et montrerons que toute formule pp, ayant ses paramètres dans cette famille, vérifie un principe local-global. Nous les baptiserons formules V-universelles. Nous clorons le dernier chapitre par deux méthodes de construction.

Th. doct.-ing.--Informatique--Nancy--I.N.P.L., 1984.