L'utilisation omniprésente des systèmes informatiques impose de s'assurer de leur bon fonctionnement. Dans ce but, les méthodes de vérification formelle permettent de suppléer les simulations qui ne peuvent être complètement exhaustives du fait de la complexité croissante des systèmes. Le model checking fait partie de ces méthodes et présente l'avantage d'être complètement automatisée. Cette méthode consiste à développer des algorithmes pour vérifier qu'une spécification exprimée la plupart du temps sous la forme d'une formule logique est satisfaite par un modèle du système. Les langages historiques de spécification utilisent comme formules atomiques des variables propositionnelles qui permettent d'exprimer principalement des propriétés portant sur les états de contrôle du modèle. Le but de cette thèse est de vérifier des propriétés plus riches portant sur diverses données manipulées par les modèles: des compteurs, des horloges ou des queues. Ces données peuvent prendre une infinité de valeurs et induisent donc des modèles avec un nombre infini d'états. Nous définissons un cadre général pour l'extension des logiques temporelles avec des contraintes permettant de comparer la valeur des variables a différents états de l'exécution. Nous établissons des résultats de décidabilité et complexité pour des problèmes de model checking impliquant diverses instances de ces extensions. Nous privilégions pour cela l'approche à base d'automates en combinant des constructions connues pour les logiques propositionnelles classiques avec des méthodes d'abstraction des modèles dont les variables sont interprétées dans des domaines infinis.

La thèse s'intéresse au problème de l'analyse syntaxique pour les langages de programmation. Si ce sujet a déjà été traité à maintes reprises, et bien que des outils performants pour la génération d'analyseurs syntaxiques existent et soient largement employés, l'implémentation de la partie frontale d'un compilateur reste encore extrêmement complexe.<br /><br />Ainsi, si le texte d'un programme informatique se doit de n'avoir qu'une seule interprétation possible, l'analyse des langages de programmation, fondée sur une grammaire algébrique, est, pour sa part, le plus souvent non déterministe, voire ambiguë. Confrontés aux insuffisances des analyseurs déterministes traditionnels, les développeurs de parties frontales se sont tournés massivement vers des techniques d'analyse générale, à même d'explorer des choix non déterministes, mais aussi au prix de la garantie d'avoir bien traité toutes les ambiguïtés grammaticales. Une difficulté majeure dans l'implémentation d'un compilateur réside alors dans l'identification (non décidable en général) et le traitement de ces ambiguïtés.<br /><br />Les techniques décrites dans la thèse s'articulent autour d'approximations des grammaires à deux fins. L'une est la génération d'a\-na\-ly\-seurs syntaxiques non canoniques, qui sont moins sensibles aux dif\-fi\-cultés grammaticales, en particulier parce qu'ils peuvent exploiter un langage algébrique non fini en guise de contexte droit pour résoudre un choix non déterministe. Ces analyseurs rétablissent la garantie de non ambiguïté de la grammaire, et en sus assurent un traitement en temps linéaire du texte à analyser. L'autre est la détection d'ambiguïté en tant que telle, avec l'assurance qu'une grammaire acceptée est bien non ambiguë quel que soit le degré d'approximation employé.

Dans cette thèse, nous étudions des modèles d'agrégation limitée, qui modélisent la coalescence de particules ayant des "bras", c'est-à-dire un nombre fixé de liens potentiels. Une particule ne peut donc créer plus de liens que son nombre de bras. On s'intéresse en particulier à une variante de l'équation de Smoluchowski introduite par Jean Bertoin. Ce document comprend, outre l'introduction, trois chapitres. Le premier est dévolu à l'étude d'un modèle sexué de coagulation, où les particules ont des bras mâles et femelles et seuls des bras de sexes opposés peuvent se joindre. Ce modèle généralise et unifie ceux de Bertoin, dont on peut en particulier retrouver les résultats. Le second chapitre comprend un travail en collaboration avec Lorenzo Zambotti. On s'y intéresse à l'unicité des solutions d'équations de coagulation après gélification, en particulier l'équation de Smoluchowski avec noyau multiplicatif et l'équation d'agrégation limitée. En particulier, on donne des preuves rigoureuses de certaines heuristiques de la littérature physique, par exemple en calculant précisément le temps de gélification. Dans le cas d'agrégation limitée, on obtient aussi des formules particulièrement simples pour les concentrations limites. Pour expliquer celles-ci, on étudie dans le dernier chapitre un modèle microscopique pour l'équation de Smoluchowski d'agrégation limitée. Ceci est un travail commun avec Mathieu Merle. On parvient à décrire précisément l'état microscopique du système à tout temps et ainsi à retrouver les formules du second chapitre. Une caractéristique frappante de ce modèle est qu'il possède une propriété de criticalité auto-organisée.