Ce travail s'intéresse à la preuve de propriétés de sûreté sur les programmes. Prouver de telles propriétés revient généralement à démontrer que les configurations critiques ne sont jamais atteintes lors de l'exécution du programme. Pour ces propriétés, nous proposons une technique de vérification semi-automatique qui tente de combiner les avantages du model-checking, interprétation abstraite et preuve interactive. Comme en model-checking, cette technique permet de prouver automatiquement des propriétés de sûreté sur les systèmes finis, ainsi que sur certaines classes de systèmes infinis ayant une présentation finie. En dehors de ces classes et comme en interprétation abstraite, notre technique permet d'approcher le comportement infini d'un système par une sur-approximation sûre. Enfin, lorsque les approximations sont trop grossières, il nous est possible d'intervenir manuellement sur la définition des approximations afin de les raffiner et, si cela est possible, de mener la preuve à son terme. Cette approche est basée sur les systèmes de réécriture qui sont un des outils centraux de la déduction automatique. Nous les utilisons comme formalisme pour représenter les programmes: une configuration de programme est représentée par un terme et les transitions entre configurations par des règles de réécriture. Sur de tels modèles, prouver la sûreté d'un programme revient à faire une analyse d'atteignabilité, c.-à-d. vérifier que les termes représentant les configurations critiques sont inatteignables par réécriture des termes initiaux. L'ensemble des termes atteignables est représenté par un automate d'arbre. La construction de cet automate est effectuée en utilisant un algorithme de complétion spécifique. Pour la définition des approximations, nous avons proposé deux langages spécifiques, l'un calqué sur la structure des automates et l'autre utilisant des équations sur les termes. Ce dernier permet, en particulier, d'estimer la précision des approximations construites par rapport à la réécriture modulo équations. Cette technique a été expérimentée pour la vérification de protocoles cryptographiques ainsi que pour le protoypage rapide d'analyses statiques de programmes Java byte code.

La coupe forestière s'est beaucoup intensifiée dans les dernières décennies dans la forêt boréale canadienne. L'environnement aquatique est directement affecté par les perturbations de l'environnement terrestre. Ainsi, les coupes forestières pourraient affecter l'ensemble du réseau trophique des écosystèmes lacustres et l'habitat d'alimentation de l'omble de fontaine (Salvelinus fontinalis), l'espèce sportive la plus pêchée au Québec. Cependant, il y a peu d'information traitant des effets de l'exploitation forestière sur les écosystèmes lacustres et leurs populations piscicoles. L'objectif général de ce projet était d'évaluer l'impact des coupes forestières sur le fonctionnement du réseau trophique de l'omble de fontaine dans des lacs de la forêt boréale. Les objectifs spécifiques poursuivis visaient à (1) réaliser une description isotopique de la structure du réseau trophique de l'omble de fontaine avant la coupe forestière ; (2) évaluer l'impact des coupes forestières sur la qualité de l'eau et sur la nature du carbone organique dissous et (3) évaluer l'impact des coupes forestières sur le réseau trophique lacustre et sur l'omble de fontaine basé sur l'analyse des signatures isotopiques du carbone et de l'azote. Pour atteindre ces objectifs, nous avons échantillonné huit lacs en forêt boréale, dans le bassin hydrographique de la Rivière Mistassibi-Est, à environ 215 km de Dolbeau-Mistassini. Les échantillons ont été collectés en juillet 2008, 2009 et 2010. Quatre lacs ont subi les effets de coupes forestières sur leur bassin versant à partir du second été d'échantillonnage (groupe coupé) et quatre autres lacs n'ont subi aucune perturbation lors de l'étude (groupe témoin). Les coupes forestières ont été menées selon la stratégie de la coupe avec protection de la régénération et des sols (CPRS). Tous les lacs ont été échantillonnés avant que ne débutent les coupes forestières (juillet 2008), puis ont été revisités après les coupes (juillet 2009 et 2010). La matière organique d'origine terrestre s'est avérée être la principale source de carbone des invertébrés benthiques dans tous les lacs échantillonnés. L'omble de fontaine dépendait principalement, quant à lui, des macroinvertébrés benthiques prédateurs pour son alimentation (objectif 1). Les activités de coupes forestières semblent avoir un impact à court terme (i.e., une année après la perturbation) sur les concentrations en carbone organique dissous et en phosphore total (objectif 2). Il apparaît cependant que cet impact est atténué deux ans après la perturbation, ce qui suggère que le système lacustre est résilient et donc en mesure de retourner au stade initial. Les activités de coupes forestières n'ont pas affecté la nature du carbone organique retrouvé dans les lacs. Ce carbone est essentiellement d'origine allochtone dans tous les lacs (objectif 2). La principale source de carbone pour les consommateurs benthiques primaires est la matière organique d'origine allochtone (feuilles) autant dans les lacs témoins que les lacs coupés (objectif 3). L'omble de fontaine s'alimente principalement des invertébrés benthiques prédateurs dans les lacs témoins. Cependant, dans les lacs coupés un an après la perturbation, l'omble de fontaine semble s'alimenter principalement du zooplancton plutôt que du zoobenthos. Et deux années après la coupe, l'omble de fontaine retourne à un mode d'alimentation rencontré avant la coupe (objectif 3). Ceci ne fait que confirmer que les lacs étudiés ont une certaine résilience, étant donné que deux années après la coupe, ils sont capables de retourner au même stade qu'avant la perturbation. Ce projet de recherche a contribué à mieux comprendre les interactions de l'omble de fontaine avec les activités sur les bassins versants des lacs qui l'hébergent. Plusieurs résultats de recherche restent à être approfondis. Cependant, deux résultats peuvent contribuer à une meilleure gestion de l'omble de fontaine : (1) les écosystèmes lacustres en forêt boréale, et plus particulièrement l'omble de fontaine, dépendent indirectement de la matière organique produite par les écosystèmes forestiers riverains et (2) il existe une résilience des systèmes lacustres étudiés puisqu'ils retournent à leur état initial deux années après la coupe. Ce projet de recherche a favorisé une approche intégrée des écosystèmes terrestres et aquatiques en regard des coupes forestières en forêt boréale, une approche souvent occultée dans les études centrées sur un seul type d'écosystème. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Coupes forestières, réseau trophique, lac, forêt boréale, omble de fontaine, matière organique, isotopes stables

Les systèmes informatiques jouent un rôle essentiel dans la vie actuelle, et leurs erreurs peuvent avoir des conséquences dramatiques. Il existe des méthodes formelles permettant d'assurer qu'un système informatique est fiable. La méthode formelle utilisée dans cette thèse est appelée complétion d'automates d'arbres et permet d'analyser les systèmes à nombre d'états infini. Dans cette représentation, les états du système sont représentés par des termes et les ensembles d'états par des automates d'arbres. L'ensemble des comportements possibles d'un système est calculé grâce à l'application successive d'un système de réécriture modélisant le comportement du système vérifié. On garantit la fiabilité d'un système en vérifiant qu'un comportement interdit n'est pas présent dans l'ensemble des états accessibles. Mais cet ensemble n'est pas toujours calculable, et nous devons alors calculer une sur-approximation calculable de cet ensemble. Mais cette approximation peut s'avérer trop grossière et reconnaître de faux contre-exemples. La première contribution de cette thèse consiste alors à caractériser, par des formules logiques et de manière automatique, ce qu'est une "bonne" sur-approximation : une approximation représentant un sur-ensemble des configurations accessibles, et qui soit suffisamment précise pour ne pas reconnaître de faux contre-exemples. Résoudre ces formules conduit alors automatiquement à une sur-approximation concluante si elle existe, sans avoir recours à aucun paramétrage manuel. Le second problème de la complétion d'automates d'arbres est le passage à l'échelle, autrement dit le temps de calcul parfois élevé du calcul de complétion quand on s'attaque à des problèmes de la vie courante. Dans la vérification de programmes Java utilisant la complétion d'automates d'arbres, cette explosion peut être due à l'utilisation d'entiers de Peano. L'idée de notre seconde contribution est alors d'évaluer directement le résultat d'une opération arithmétique. D'une façon plus générale, il s'agit d'intégrer les éléments d'un domaine infini dans un automate d'arbres. En s'inspirant de méthodes issues de l'interprétation abstraite, cette thèse intègre des treillis abstraits dans les automates d'arbres, constituant alors un nouveau type d'automates. Les opérations sur le domaine infini représenté sont calculées en une seule étape d'évaluation plutôt que d'appliquer de nombreuses règles de réécriture. Nous avons alors adapté la complétion d'automates d'arbres à ce nouveau type d'automate, et la généricité du nouvel algorithme permet de brancher de nombreux treillis abstraits. Cette technique a été implémentée dans un outil appelé TimbukLTA, et cette implémentation permet de démontrer l'efficacité de cette technique.

Nous proposons deux caractérisations des arbres réguliers. La première est sémantique et s'appuie sur les types co-inductifs. La seconde est syntaxique et repose sur une représentation des arbres réguliers par des termes cycliques. Nous prouvons que ces deux caractérisations sont isomorphes.Ensuite, nous étudions le problème de la définition de morphisme d'arbres préservant la propriété de régularité. Nous montrons en utilisant le formalisme des transducteurs d'arbres, l'existence d'un critère syntaxique garantissant la préservation de cette propriété. Enfin, nous considérons des applications de la théorie des arbres réguliers comme la définition de l'opérateur de composition parallèle d'une algèbre de processus ou encore, les problèmes de décidabilité sur les arbres réguliers via une mécanisation d'un vérificateur de modèles pour un mu-calcul coalgébrique. Tous les résultats ont été mécanisés et prouvés corrects dans l'assistant de preuve Coq. / We propose two characterizations of regular trees. The first one is semantic and is based on coinductive types. The second one is syntactic and represents regular trees by means of cyclic terms. We prove that both of these characterizations are isomorphic. Then, we study the problem of defining tree morphisms preserving the regularity property. We show, by using the formalism of tree transducers, the existence of syntactic criterion ensuring that this property is preserved. Finally, we consider applications of the theory of regular trees such as the definition of the parallel composition operator of a process algebra or, the decidability problems on regular trees through a mechanization of a model-checker for a coalgebraic mu-calculus. All the results were mechanized and proved correct in the Coq proof assistant.

L’étude des automates est un sujet fondamental de l’informatique. Ce modèle apporte des solutions pratiques à divers problèmes en compilation et en vérification notamment. Dans ce travail nous proposons l'extension aux automates à pile visible de résultats existants pour les automates. Nous proposons une définition d'automate à pile visible émondé et donnons un algorithme s’exécutant en temps polynomial émondant un automate en préservant son langage. Nous donnons aussi un algorithme de complexité exponentielle qui, pour un automate à pile visible donné, construit un automate équivalent à la fois émondé et déterministe. Cette complexité exponentielle se révèle optimale. Étant donné un automate à pile visible, nous pouvons associer à ses transitions des coûts pris dans un semi-anneau S. L’automate associe ainsi un mot d’entrée à un élément de S. Le coût d’un automate est le supremum des coûts associés aux mots d'entrée. Pour les semi-anneaux des entiers naturels et Max-plus, nous donnons des caractérisations et des algorithmes polynomiaux pour décider si le coût d’un automate est fini. Puis, nous étudions pour les entiers naturels la complexité du problème de la majoration du coût par un entier k. Les transducteurs à pile visibles produisent des sorties sur chaque mot accepté. Un problème classique est de décider s'il existe une borne sur le nombre de sorties de chaque mot accepté. Pour une sous-classe des transducteurs à pile visible, nous proposons des propriétés caractérisant les instances positives de ce problème. Nous montrons leur nécessité et discutons d’approches possibles afin de montrer leur suffisance. / The study of automata is a central subject of computer science. This model provides practical solutions to several problems including compilation and verification. In this work we extend existing results of automata to visibly pushdown automata. We give a definition of trimmed visibly pushdown automata and a polynomial time algorithm to trim an automata while preserving its language. We also provide an exponential time algorithm which, given a visibly pushdown automaton, produces an equivalent automaton, both deterministic and trimmed. We prove the optimality of the complexity. Given a visibly pushdown automaton, we can equip its transitions with a cost taken from a semiring S, and thus associate each input word to an element of S. The cost of the automaton is the supremum of the input words cost. For the semiring of natural integers and Max-plus, we give characterisations and polynomial time algorithms to decide if the cost of a visibly pushdown automaton is finite. Then in the case of natural integers we study the complexity of deciding if the cost is bounded by a given integer k. Visibly pushdown transducers produce output on each accepted word. A classical problem is to decide if there exists a bound on the number of outputs of each accepted word. In the case of a subclass of visibly pushdown transducers, we give properties characterizing positive instances of this problem. We show their necessity and discuss of possible approaches to prove their sufficiency.

Le papier cherche à mesurer l'importance de l'effet du resquillage dans le travail d'équipe. La littérature existante présente de manière théorique les facteurs susceptibles d'augmenter le resquillage, sans toutefois quantifier son impact. Hamilton et al. (2003) ont observé la productivité des employés selon qu'ils travaillaient seuls ou en équipes. Cependant, ils ne sont pas parvenus à séparer l'effet du resquillage des autres caractéristiques du travail d'équipe. Notre papier se base sur une expérience réalisée sur les planteurs d'arbres. Nous avons observé la productivité des employés quand ils travaillaient individuellement et en équipe de deux personnes. Ce type de travail possède des caractéristiques qui facilitent la comparaison du rendement des employés entre les deux situations. Les travailleurs n'ont pas exploité l'opportunité de profiter des efforts de l'autre. L'effet du resquillage s'avère inexistant. Un effet important de resquillage pourrait encourager les employeurs à privilégier le travail individuel au détriment du travail d'équipe.

Les travaux de sous-solage qui améliorent le drainage interne et décompactent des horizons rendus pratiquement imperméables par la compaction profonde seraient bénéfiques aux sols de faible perméabilité. Le sous-solage profond exécuté perpendiculairement aux drains avec un bélier (bulldozer) pourrait être plus efficace pour temporairement améliorer le drainage de ces sols qu’une sous-soleuse conventionnelle attelée à un tracteur et opérée en mode parallèle aux drains. Toutefois, les aménagements réalisés pour améliorer le drainage de surface et interne de ces sols rendent complexe l’évaluation de ces pratiques en dispositif expérimental. L’objectif principal de ce projet était de comparer les forêts d’arbres décisionnelles (FAD) à la régression linéaire multiple (RLM) pour détecter les effets du sous-solage et des systèmes de drainage souterrain et de surface sur la hauteur des plants et la profondeur moyenne de la nappe durant la saison de croissance. Un essai de sous solage a été réalisé à l’automne 2014, dans une argilelimoneuse Kamouraska naturellement mal drainée, remodelée en planches arrondies et souffrant de compaction importante. L’essai comparait un témoin sans sous-solage à quatre traitements de sous-solage, soit une sous-soleuse sur bélier ou sur tracteur, opérées parallèlement ou perpendiculairement aux drains. Chaque traitement a été répété trois fois et disposé aléatoirement en autant de blocs. Au printemps 2016, 198 puits ont été creusés à 60 cm de profondeur pour enregistrer la profondeur de la nappe sous chaque traitement entre juin et juillet 2016. La photogrammétrie a été utilisée pour estimer la hauteur des plants de maïs. Les FAD et la RLM permettent de détecter les principaux facteurs affectant la hauteur des plants de maïs et la profondeur moyenne de la nappe, soit les aménagements antérieurs pour améliorer le drainage interne et le drainage de surface des sols. Les coefficients de détermination obtenus avec les FAD (R2 ≥ 0,94) étaient toutefois plus élevés que ceux obtenus avec la RLM (R2 ≥ 0,28). Aucun traitement de sous-solage n’a amélioré significativement le drainage interne ni la hauteur des plants de maïs par rapport au témoin sans sous-solage. Les FAD permettent en outre de mieux visualiser les relations non linéaires entre les variables prédites et les autres variables, notamment la position sur la planche et la distance aux drains souterrains, et finalement de déterminer les distances aux drains souterrains optimales (< 2 m) et critiques (> 4 m), la distance optimale à la raie de curage (> 8 m) et la profondeur moyenne critique de la nappe (< 0,25 m). Les FAD permettent ainsi de prédire la hauteur des plants de maïs et la profondeur moyenne de la nappe avec une plus grande précision qu’avec la RLM.

Cette thèse traite de la révision automatique des connaissances contenues dans les systèmes fonctionnant par exploration informée d'arbres d'états. Ces systèmes, de par leur performance, sont employés dans de nombreux domaines applicatifs. En particulier, des travaux ont proposés d’utiliser cette approche dans le cadre de l'automatisation de la généralisation de données géographiques. La généralisation de données géographique s'intéresse à la dérivation, à partir de données géographiques détaillées, de données moins détaillées adaptées à un besoin particulier (e.g. changement d'échelle). Son automatisation, enjeu majeur pour les agences cartographiques telles que l'Institut Géographique National (IGN), est particulièrement complexe. Les performances des systèmes basés sur l’exploration informée d'arbres d'états sont directement dépendantes de la qualité de leurs connaissances (heuristiques). Or, la définition et la mise à jour de ces dernières s'avèrent généralement fastidieuses. Dans le cadre de cette thèse, nous proposons une approche de révision hors ligne des connaissances basée sur le traçage du système et sur l'analyse de ces traces. Ces traces sont ainsi utilisées par un module de révision qui est chargé d'explorer l'espace des connaissances possibles et d'en modifier en conséquence les connaissances du système. Des outils de diagnostic en ligne de la qualité des connaissances permettent de déterminer quand déclencher le processus de révision hors ligne des connaissances. Pour chaque méthode et approche que nous présentons, une mise en oeuvre est détaillée et expérimentée dans le cadre de l'automatisation de la généralisation de données géographiques / This work deals with automatic knowledge revision in systems based on an informed tree search strategy. Because of their efficiency, these systems are used in numerous fields. In particular, some literature work uses this approach for the automation of geographic data generalisation. Geographic data generalisation is the process that derives data adapted to specific needs (e.g. map scale) from too detailed geographic data. Its automation, which is a major issue for national mapping agencies like Institut Géographique National (IGN), is particularly complex. The performances of systems based on informed tree search are directly dependant on their knowledge (heuristics) quality. Unfortunately, most of the time, knowledge definition and update are fastidious. In this work, we propose an offline knowledge revision approach based on the system logging and on the analysis of these logs. Thus, the logs are used by a revision module which is in charge of the system knowledge revision by knowledge space exploration. Tools for online knowledge quality diagnosis allow to determine when the offline knowledge process should be activated. For each method and each approach presented, an implementation is proposed in the context of geographic data generalisation

La première partie aborde la conception et la mise en œuvre d'un outil d'analyse syntaxique capable de manipuler des informations syntaxiques et sémantiques. La problématique de l'analyse d'une langue naturelle est d'abord présentée: nous essayons de montrer quels sont les invariants de quelques formalismes récents et comment ces invariants ont motive nos choix. Nous décrivons ensuite le constructeur de structures de dépendances que nous proposons et les apports d'une hiérarchie de catégories a la souplesse et a la tolérance de l'analyse. Les arbres de dépendances produits sont décores grâce a un formalisme de représentation de la connaissance base sur des structures de traits intégrant un mécanisme d'héritage. Nous terminons en présentant le prototype d'analyseur que nous avons réalisé. La deuxième partie définit une architecture pour un système de détection et de correction qui exploite de manière cohérente tous les outils dont nous disposons. Les outils de niveau lexical comprennent un analyseur et un générateur morphologiques et des modules de correction lexicale utilisant trois techniques: phonétique, morphologie et clé squelette. Après avoir décrit les objectifs fixes pour le niveau syntaxique, nous donnons un aperçu du vérificateur syntaxique dont nous disposons et nous soulignons les apports des concepts et outils de la première partie a la robustesse des traitements. Enfin, nous proposons l'architecture d'un système complet de détection et correction d'erreurs dans un texte écrit en insistant sur sa portabilité et son adaptabilité.

Cette thèse s'inscrit dans le domaine du traitement automatique des langues naturelles et plus spécifiquement dans celui du traitement du vietnamien. Le travail présenté dans la thèse porte sur la construction d'outils et de ressources linguistiques pour les tâches fondamentales de traitement automatique du vietnamien, notamment la construction d'une grammaire à large couverture et un analyseur syntaxique pour cette langue. Nous développons une chaîne modulaire de prétraitements pour le vietnamien dont le rôle est d'appliquer à des corpus bruts une cascade de traitements de surface. Il s'agit d'un segmenteur en phrases, d'un segmenteur en unités lexicales, d'un reconnaisseur de mots redoublés et d'un étiqueteur morpho-syntaxique. Préalables nécessaires à une possible analyse, ces traitements peuvent également servir à préparer d'autres tâches. La modélisation de la grammaire vietnamienne est effectuée en utilisant le formalisme des grammaires d'arbres adjoints lexicalisées (Lexicalized Tree Adjoining Grammars ou LTAG). Nous développons un système qui extrait automatiquement une grammaire LTAG à partir d'un corpus arboré du vietnamien. Les arbres élémentaires de la grammaire forment les structures syntaxiques de la langue vietnamienne. Nous adaptons et enrichissons un analyseur syntaxique du français pour construire un analyseur syntaxique profond pour le vietnamien. Nous présentons les fondements théoriques des différents modules et systèmes, leurs évaluations quantitatives. Nos systèmes atteignent des performances prometteuses dans les tâches du traitement automatique du vietnamien à l'heure actuelle.