Cette thèse est consacrée au développement de méthodes formelles pour la vérification de logiciels. Parmi les techniques les plus utilisées dans ce contexte, il y en a deux qui permettent une spécification rigoureuse de toutes les exécutions possibles d'un système et le contrôle des bogues cachés. D'un côté, la correction d'un programme peut être garantie en démontrant l'insatisfiabilité d'une formule modulo une théorie qui axiomatise les types de données impliqués; de l'autre côté, les techniques de model-checking sont utilisées pour certifier que toute exécution possible du système satisfait les propriétés désirées. Les contributions de cette thèse sont les suivantes. Dans un premier temps, nous donnons un résultat de décidabilité pour la satisfiabilité de contraintes pour des extensions intéressantes de la théories des tableaux. Ensuite, nous avons obtenu des résultats dans le prolongement de Manna et Pnueli qui ont montré qu'un mélange de la logique du premier ordre et de la logique temporelle linéaire suffit pour énoncer les problèmes de vérification pour la classe des systèmes réactifs. Ainsi, nous nous inspirons de la récente littérature sur la combinaison des procédures de décision pour établir des résultats de décidabilité et d'indécidabilité pour le problème de satisfiabilité pour des logiques permettant d'intégrer du raisonnement modulo des théories du premier ordre dans un cadre temporel. Les résultats qu'on obtient pour la logiques temporelle linéaire sont ensuite généralisés au cas où le flux temporel est décrit par une logique dont le problème de la satisfiabilité relativisée est décidable. Notre dernière contribution est la décidabilité du problème du model-checking pour le flux temporel linéaire, sous des hypothèses appropriées concernant les théories du premier ordre impliquées. La preuve de ce résultat indique qu'on pourrait employer avec succès des Solveurs Modulo des Théories dans les applications du model-checking aux systèmes ayant un nombre infini d'états. / The thesis is devoted to the development of formal methods for software verification. Indeed, two are among the most widespread techniques that allow to rigorously specify the possible executions of a system and check whether it contains bugs. On the one hand, correctness of a program can be guaranteed by showing the unsatisfiability of a formula modulo a theory which usually axiomatizes the involved datatypes; on the other hand, model checking techniques are used to certify that every possible run of the system satisfies the desired properties. The contributions of the thesis are the following: First of all, we give decidability result for the constraint satisfiability problem for interesting extensions of the theory of arrays. Secondly, along the lines of Manna and Pnueli, who have shown how a mixture of first-order logic and linear time temporal logic is sufficient to state verification problems for the class of reactive systems, we draw on the recent literature about combination of decision procedures to give decidability and undecidability results for the satisfiability problem for logics that allow to plug reasoning modulo first-order theories into a temporal setting. The results obtained in the case of linear flows of time are then generalized to temporal and modal logics whose relativized satisfiability problem is decidable. The last contribution is the decidability of the model checking problem for linear flows of time under suitable hypothesis over the first-order theories involved. The proofs of the decidability results suggest that efficient Satisfiability Modulo Theories solvers might be successfully employed in the model checking of infinite-state systems.

Th.--Méd.--Paris, 1853. / Voyez tome , page . N ° . Paris, 1853. Thèse de Concours.

La thèse étudie des problèmes de vérification de modèles infini, en appliquant des techniques de combinaisons de solveurs de contraintes.

Beaucoup d'applications des méthodes formelles reposent sur la génération de formules en logique du premier ordre et la preuve de leur satisfiabilité par rapport à une théorie en arrière-plan, qui est souvent obtenu par mélange de plusieurs théories. Dans la littérature, cette forme de satisfiabilité est appelée Satisfiabilité Modulo Théories (SMT). Dans cette thèse, on s'intéresse à la conception de procédures de décision pour les problèmes SMT, en intégrant des techniques de saturation basées sur la réécriture pour des théories finiment axiomatisées et des techniques de combinaison pour des unions de théories. La première contribution de cette thèse est une reconstruction raisonnée, dans un cadre uniforme, des méthodes de combinaison proposées par Nelson-Oppen, Shostak et d'autres. Ceci est le point de départ pour de nouvelles investigations. Nous introduisons ensuite le concept de canoniseur étendu et dérivons un résultat de modularité pour une nouvelle classe de théories, ce qui contraste avec l'absence de modularité pour la classe de théories considérée par Shostak. La deuxième contribution concerne le problème de la combinaison de procédures basées sur la réécriture en utilisant la méthode de Nelson-Oppen. Nous utilisons la méta-saturation pour développer des techniques de preuve automatique permettant de tester les conditions pour la combinabilité de telles procédures. Lorsque la méta-saturation termine pour une théorie, le résultat obtenu permet de raisonner sur la combinabilité pour cette théorie d'une procédure de satisfiabilité basée sur la réécriture. La troisième contribution de cette thèse est liée à l'intégration des procédures de décision dans les solveurs SMT. Nous considérons le problème de rajouter aux procédures de décision la capacité de construire des justifications en cas d'insatisfiabilité, sans dégradation des performances, en nous focalisant sur la construction modulaire de telles justifications pour une théorie combinée. Pour ce faire, nous étendons la méthode de combinaison de Nelson-Oppen de manière à construire de façon modulaire des justisfications d'insatisfiabilité pour des unions de théories. Nous étudions également comment les justifications obtenues peuvent être reliées à une forme appropriée de minimalité.

Le relevé extérieur d'ouvrage architectural est le moyen de créer une représentation du bâtiment dans son état de conservation. Deux techniques d'acquisition à distance se distinguent par leur efficacité et la qualité des données produites : la photogrammétrie et le balayage optique. Ces deux techniques sont soumises aux règles de l'optique et ne permettent pas de mesurer les parties invisibles de l'objet. La combinaison des techniques peut améliorer la qualité des données, mais il subsiste toujours des zones non mesurées et de ce fait non représentables. Pour palier ce problème, nous émettons l'hypothèse que l'usage de connaissances architecturales peut permettre de recomposer les parties manquantes lors de la modélisation. Cette thèse propose un processus basé sur la combinaison de ces deux techniques et sur l'intégration des connaissances architecturales accessibles depuis la documentation écrite ou encore par les règles de construction des édifices. La complexité d'un ouvrage architectural et la multitude des données imposent une division de la modélisation en plusieurs étapes identifiables. Nous proposons de découper le processus de modélisation selon le mode de figuration des niveaux de détail utilisé pour la représentation de l'architecture. Les niveaux différents de détail permettent d'obtenir des étapes de modélisation clairement indentifiables, mais aussi un processus progressif où les informations peuvent être utilisées au fur et à mesure. Notre approche intègre ainsi les données dimensionnelles à la documentation architecturale, pour permettre la mise en place d'un processus de modélisation afin d'obtenir un modèle le plus complet possible

Lorsque plusieurs classifieurs sont amenés à concourir à une même tâche de reconnaissance, plusieurs stratégies de décisions, impliquant ces classifieurs de différents manières, sont possibles. Une première stratégie consiste à décider suite à différents avis : il s'agit de la combinaison de classifieurs. Une deuxième stratégie consiste à utiliser un ou plusieurs avis pour mieux guider d'autres classifieurs dans leurs phases d'apprentissages, et à utiliser un ou plusieurs avis pour améliorer la prise de décisions d'autres classifieurs dans la phase de classement : il s'agit de la coopération de classifieurs. Enfin, la troisième et dernière stratégie consiste à privilégier un ou plusieurs classifieurs en fonction de divers critères ou en fonction de la situation : il s'agit de la sélection de classifieurs. L'aspect temporel de la RdF, c'est-à-dire l'évolution possible des classes à reconnaître, est traité par la stratégie de la sélection. En étudiant les aspects statiques et dynamiques de la RdF, nous montrons que pour reconnaître des classes dynamiques, deux approches sont possibles. Ces deux approches sont validées sur un ensemble de test. Dans le cas où les trajectoires des classes ne s'intersectent pas et que ces classes sont multimodales, l'approche proposée consiste à transformer ces classes dynamiques en classes statiques. En intégrant l'évolution de ces classes dans le temps, les classes obtenues deviennent alors complexes. Pour traiter ce type de classes, un algorithme de coopération des classifieurs est proposé. Il met en {\oe}uvre, d'une part, une méthode de classification non-supervisée effectuant une sélection adaptative de classifieurs et, d'autre part, plusieurs méthodes de RdF supervisées. Lorsqu'il n'y a pas d'intersection et que les classes évoluent de manière continue dans le temps, l'approche proposée consiste à rendre dynamique le système de RdF. Une méthode, fondée sur la modélisation des changements d'états du système par un réseau de Petri flou, est proposée. La méthode permet de prédire le ou les états du système les mieux adaptés au problème de RdF, à l'instant considéré.

Les propriétés intrinsèques de la fibre optique utilisée comme milieu à gain en font un candidat idéal pour le développement de sources laser de haute puissance, aujourd'hui capable de rivaliser avec les lasers à état solide, tout en apportant ses avantages propres : robustesse, efficacité, qualité de faisceau potentielle, gestion de la thermique, compacité et tenue à l'environnement. Les domaines d'application sont nombreux : industrie (usinage, marquage), défense (télémétrie, imagerie), environnement (lidar), communications en espace libre, recherche fondamentale... Cependant, certaines applications nécessitent des puissances ou énergie encore supérieures à ce que peut délivrer une seule fibre associée à une bonne qualité de faisceau. Pour contourner cette difficulté, l'approche abordée ici est de répartir l'amplification sur plusieurs fibres lasers, puis de recombiner les faisceaux en espace libre. Ce travail est préparatoire à une nouvelle génération de lasers hyper-intenses et a été réalisé dans le cadre du projet ANR CAN, collaboration entre LOA, IOGS, Thales R&T et Onera. Suivant le dimensionnement défini par l'étude théorique de la combinaison cohérente de faisceaux laser, un toron de 64 fibres collimatées chacune par une petite lentille est conçu puis réalisé technologiquement. Par extension de l'idée de l'interféromètre à décalage quadri-latéral, une méthode de mesure collective et auto-référencée de la phase des fibres est mise au point. Enfin, une technique originale et auto-adaptative de mise en phase par holographie numérique est présentée et validée expérimentalement.

La fusion d'informations issues de plusieurs sources cherche à améliorer la prise de décision. Pour réaliser cette fusion, la théorie des fonctions de croyance utilise des règles de combinaison faisant bien souvent l'hypothèse de l'indépendance des sources. Cette forte hypothèse n'est, cependant, ni formalisée ni vérifiée. Elle est supposée pour justifier le choix du type de règles à utiliser sans avoir, pour autant, un moyen de la vérifier. Nous proposons dans ce rapport de thèse un apprentissage de l'indépendance cognitive de sources d'information. Nous détaillons également une approche d'apprentissage de la dépendance positive et négative des sources. Les degrés d'indépendance, de dépendance positive et négative des sources ont principalement trois utilités. Premièrement, ces degrés serviront à choisir le type de règles de combinaison à utiliser lors de la combinaison. Deuxièmement, ces degrés exprimés par une fonction de masse sont intégrés par une approche d'affaiblissement avant de réaliser la combinaison d'information. Une troisième utilisation de cette mesure d'indépendance consiste à l'intégrer dans une nouvelle règle de combinaison. La règle que nous proposons est une moyenne pondérée avec ce degré d'indépendance. / The theory of belief functions manages uncertainty and proposes a set of combination rules to aggregate beliefs of several sources. Some combination rules mix evidential information where sources are independent; other rules are suited to combine evidential information held by dependent sources. Information on sources ' independence is required to justify the choice of the adequate type of combination rules. In this thesis, we suggest a method to quantify sources' degrees of independence that may guide the choice of the appropriate type of combination rules. In fact, we propose a statistical approach to learn sources' degrees of independence from all provided evidential information. There are three main uses of estimating sources' degrees of independence: First, we use sources' degree of independence to guide the choice of combination rules to use when aggregating beliefs of several sources. Second, we propose to integrate sources' degrees of independence into sources' beliefs leading to an operator similar to the discounting. Finally, we define a new combination rule weighted with sources' degree of independence.

Des études récentes montrent une part croissante de requêtes sur les moteurs de recherche du Web comportant des critères géographiques. Cette part est encore plus conséquente sur des corpus plus spécifiques tels que des documents patrimoniaux (récits de voyages par exemple). On admet que l'information géographique est composée de trois facettes : le spatial, le temporel et le thématique. Les travaux effectués dans notre laboratoire visent l'extraction et la construction d'index indépendants et spécifiques aux trois facettes (spatiales, temporelles et thématiques). L'objet de ce travail de thèse est de combiner les trois facettes pour effectuer des recherches multicritère. Ce travail s'intègre au croisement de plusieurs disciplines : Traitement Automatique des Langages Naturels (TALN), Systèmes d'Information Géographique (SIG), Recherche d'Information classique (RI) et Recherche d'Information Géographique (RIG). Notre première contribution porte sur une méthode originale de combinaison des index spécifiques. Lors de l'interrogation il s'agit de questionner de manières indépendantes les différents index puis de combiner les listes de résultats restitués lors de leur interrogation. De plus, nous proposons à un utilisateur de personnaliser cette combinaison par des contraintes. Pour pouvoir effectuer cette combinaison, nous proposons d'imiter les approches d'homogénéisation utilisées dans les stratégies de RI classiques portant sur des termes et les lemmes correspondants. Pour les informations géographiques il s'agit de les redécouper en tuiles et de travailler sur leur fréquence d'apparition. Notre deuxième contribution porte sur une approche d'uniformisation générique mise en œuvre sur l'information spatiale et l'information temporelle. Afin d'évaluer ces différentes propositions, nous les avons testées et validées via différents prototypes et expérimentations. La dernière contribution consiste en un cadre d'évaluation d'un système de recherche géographique. Grâce à ce cadre nous avons pu vérifier et quantifier l'apport de la combinaison de critères géographiques ainsi que comparer différentes approches de combinaisons.

Les travaux décrits dans ce document ont pour objectif le développement de procédures de décision (et de résolution) pour la vérification. La logique considérée est la logique du premier ordre avec égalité. Cette logique est évidemment indécidable en général, mais l'étude de fragments intéressants pour la vérification peut conduire à des outils automatiques de type "presse-bouton". La notion d'égalité est particulièrement intéressante pour programmer, par orientation des égalités, c'est-à-dire par réécriture, ou pour prouver, grâce au principe de remplacement d'égal par égal. Dans une modélisation en logique du premier ordre avec égalité, on est très facilement amené à utiliser simultanément plusieurs théories différentes pour représenter par exemple les fonctions et la mémoire d'un programme ainsi que les opérations arithmétiques effectuées par le programme. On se retrouve ainsi naturellement face à un problème exprimé dans un mélange de théories, qu'il est souhaitable de résoudre de façon modulaire en réutilisant les procédures de décision connus pour les théories composant le mélange. Cette problématique est au coeur de mes travaux. L'originalité de mon approche consiste à développer des méthodes de combinaison pour les procédures de décision utilisées dans le domaine de la vérification. Toutes les procédures de décision obtenues ont été évidemment élaborées en suivant une démarche de conception sûre, qui s'appuie sur une description à base de systèmes d'inférence pour faciliter leurs preuves.