Dans ce travail, on explique quelques résultats de base en théorie des D-modules arithmétiques de Berthelot. Parmi ces résultats, un résultat important est un théorème de comparaison avec la théorie des D-modules p-adiques introduite par Mebkhout et Narvaez-Maccarro. Ce résultat intervient dans des travaux récents de Caro, pour démontrer les conjectures de Berthelot sur les D-modules arithmétiques holonomes munis d'un Frobenius. Un autre résultat concerne un analogue, dans le cadre arithmétique, du théorème de Beilinson-Bernstein concernant les D-modules.

Dans la première partie de cette thèse, nous étudions un modèle de marche aléatoire centrifuge. Nous démontrons une loi du logarithme itéré pour sa norme, et nous obtenons la loi asymptotique des fluctuations de sa direction. Nous donnons ensuite un encadrement du taux de décroissance exponentielle de la probabilité qu'elle se trouve à l'instant n dans un compact fixé en montrant que la probabilité qu'une marche aléatoire centrée classique retourne dans un compact à l'instant n sans quitter un cône ne décroît pas à vitesse exponentielle. Dans la seconde partie, nous étudions le mouvement brownien de dimension quelconque, conditionné à rester dans un cône de révolution pendant une unité de temps, et nous en déduisons un principe d'invariance pour une marche aléatoire conditionnée à rester dans un cône.

Nous étudions les propriétés stochastiques de systèmes dynamiques quasi-hyperboliques.

Cette thèse, composée de trois parties, est centrée sur l'application du calcul de \text{Malliavin} à différents domaines de l'analyse stochastique, tels que les théorèmes limites, le calcul stochastique fractionnaire et la régularité des solutions d'équations différentielles stochastiques. La première partie porte sur l'étude asymptotique de modèles de regression fractionnaire et fait appel au calcul stochastique par rapport au mouvement Brownien fractionnaire et au calcul de Malliavin. La deuxième partie est centrée sur la méthode de Stein sur l'espace de Wiener et présente des résultats ayant attrait aux théorèmes limites pour des fonctionnelles de champs Gaussiens (processus moyenne mobile à mémoire longue, sommes autonormalisées) ainsi que des résultats portant sur des propriétés de déconvolution de la loi Gamma. La troisième et dernière partie a pour objet l'étude, par le calcul de Malliavin, des solutions d'équations différentielles stochastiques rétrogrades, et en particulier l'existence de densité ainsi que d'estimées de densité pour ces solutions.

Cette thèse a pour objet l'étude de processus aléatoires en milieu aléatoire. Ce type de processus a été introduit pour la première fois en 1965 par A.A. Chernov, et a depuis fait l'objet de nombreuses recherches. Parallèlement au modèle élémentaire unidimensionnel ́etudié par A.A. Chernov, de nombreuses tentatives ont ́eté faites récemment afin d'appliquer le même type d'approche dans des contextes différents. Nous nous focalisons particulièrement sur deux exemples. Tout d'abord nous étudions le cas de la marche aléatoire en milieu aléatoire sur les arbres, pour laquelle nous étendons un critère de récurrence/transience dû à R. Lyons et R. Pemantle, avant de présenter une étude du comportement asymptotique dans le régime critique. Nous montrons dans un premier cas un théorème central limite, et dans un second nous identifions un équivalent en (logn)^3. Le régime intermédiaire entre ces deux comportements a fait l'objet de travaux plus anciens de Y. Hu et Z. Shi. Dans une autre partie nous étudions un processus aléatoire en milieu aléatoire à temps continu, connu sous le nom de diffusion de Brox. Nous étendons à ce processus des résultats dûs à A. Fribergh, N. Gantert et S. Popov concernant l'accélération et le ralentissement.

.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Le travail présenté dans cette thèse est une contribution aux méthodes formelles de spécification et de vérification. Les spécifications formelles sont utilisées pour décrire un logiciel, ou plus généralement un système, d'une manière mathématique sans ambiguïté. Des techniques de vérification formelle sont définies sur la base de ces spécifications afin d'assurer l'exactitude d'un système donné. Cependant, les méthodes formelles ne sont souvent pas pratiques et facile à utiliser dans des systèmes réels. L'une des raisons est que de nombreux formalismes de spécification ne sont pas assez riches pour couvrir à la fois les exigences orientées données et orientées comportement. Certains langages de spécification ont été proposés pour couvrir ce genre d'exigences. Le langage Circus se distingue parmi ces langues par une syntaxe et une sémantique riche et complètement intégrées.L'objectif de cette thèse est de fournir un cadre formel pour la spécification et la vérification de systèmes complexes. Les spécifications sont écrites en Circus et la vérification est effectuée soit par des tests ou par des preuves de théorèmes. Des environnements similaires de spécification et de vérification ont déjà été proposés dans la littérature. Une spécificité de notre approche est de combiner des preuves de théorème avec la génération de test. En outre, la plupart des méthodes de génération de tests sont basés sur une caractérisation syntaxique des langages étudiés. Notre environnement est différent car il est basé sur la sémantique dénotationnelle et opérationnelle de Circus. L'assistant de preuves Isabelle/HOL constitue la plateforme formelle au-dessus de laquelle nous avons construit notre environnement de spécification et de vérification.La première contribution principale de notre travail est l'environnement formel de spécification et de preuve Isabelle/Circus, basé sur la sémantique dénotationnelle de Circus. Sur la base d’Isabelle/HOL nous avons fourni une intégration vérifiée d’UTP, la base de la sémantique de Circus. Cette intégration est utilisée pour formaliser la sémantique dénotationnelle du langage Circus. L'environnement Isabelle/Circus associe à cette sémantique des outils de parsing qui aident à écrire des spécifications Circus. Le support de preuve d’Isabelle/HOL peut être utilisé directement pour raisonner sur ces spécifications grâce à la représentation superficielle de la sémantique (shallow embedding). Nous présentons une application de l'environnement à des preuves de raffinement sur des processus Circus (impliquant à la fois des données et des aspects comportementaux).La deuxième contribution est l'environnement de test CirTA construit au-dessus d’Isabelle/Circus. Cet environnement fournit deux tactiques de génération de tests symboliques qui permettent la vérification de deux notions de raffinement: l'inclusion des traces et la réduction de blocages. L'environnement est basé sur une formalisation symbolique de la sémantique opérationnelle de Circus avec Isabelle/Circus. Plusieurs définitions symboliques et tactiques de génération de test sont définies dans le cadre de CirTA. L'infrastructure formelle permet de représenter explicitement les théories de test ainsi que les hypothèses de sélection de test. Des techniques de preuve et de calculs symboliques sont la base des tactiques de génération de test. L'environnement de génération de test a été utilisé dans une étude de cas pour tester un système existant de contrôle de message. Une spécification du système est écrite en Circus, et est utilisé pour générer des tests pour les deux relations de conformité définies pour Circus. Les tests sont ensuite compilés sous forme de méthodes de test JUnit qui sont ensuite exécutées sur une implémentation Java du système étudié. / The work presented in this thesis is a contribution to formal specification and verification methods. Formal specifications are used to describe a software, or more generally a system, in a mathematical unambiguous way. Formal verification techniques are defined on the basis of these specifications to ensure the correctness of the resulting system. However, formal methods are often not convenient and easy to use in real system developments. One of the reasons is that many specification formalisms are not rich enough to cover both data-oriented and behavioral requirements. Some specification languages were proposed to cover this kind of requirements. The Circus language distinguishes itself among these languages by a rich syntax and a fully integrated semantics.The aim of this thesis is to provide a formal environment for specifying and verifying complex systems. Specifications are written in Circus and verification is performed either by testing or by theorem proving. Similar specifications and verification environment have already been proposed. A specificity of our approach is to combine supports for proofs and test generation. Moreover, most test generation methods are based on a syntactic characterization of the studied languages. Our proposed environment is different since it is based on the denotational and operational semantics of Circus. The Isabelle/HOL theorem prover is the formal platform on top of which we built our specification and verification environment.The first main contribution of our work is the Isabelle/Circus specification and proof environment based on the denotational semantics of Circus. On top of Isabelle/HOL we provide a machine-checked shallow embedding of UTP, the semantics basis of Circus. This embedding is used to formalize the denotational semantics of the Circus language. The Isabelle/Circus environment associates to this semantics some parsing facilities that help writing Circus specifications. The proof support of Isabelle/HOL can be used directly to reason on these specifications thanks to the shallow embedding of the semantics. We present an application of the environment to refinement proofs on Circus processes (involving both data and behavioral aspects). The second main contribution is the CirTA testing framework build on top of Isabelle/Circus. The framework provides two symbolic test generation tactics that allow checking two notions of refinement: traces inclusion and deadlocks reduction. The framework is based on a shallow symbolic formalization of the operational semantics of Circus using Isabelle/Circus. Several symbolic definition and test generation tactics are defined in the CirTA framework. The formal infrastructure allows us to represent explicitly test theories as well as test selection hypothesis. Proof techniques and symbolic computations are the basis of test generation tactics. The test generation environment was used for a case study to test an existing message monitoring system. A specification of the system is written in Circus, and used to generate tests following the defined conformance relations. The tests are then compiled in forms of JUnit test methods and executed against a Java implementation of the monitoring system.This thesis is a step towards, on one hand, the development of sophisticated testing tools making use of proof techniques and, on the other hand, the integration of testing and proving within formally verified software developments.

Cette thèse porte sur la propagation et le retournement temporel des ondes dans des guides d'ondes aléatoirement perturbés. L'étude de la propagation dans les guides d'ondes aléatoires est devenue indispensable face au grand nombre de situations pouvant se modéliser de cette manière : comme par exemple en télécommunication, en acoustique sous-marine ou en géophysique. Le travail présenté dans cette thèse se décompose en trois chapitres. Dans un premier chapitre, on s'intéresse à la propagation des ondes dans un guide d'onde océanique inhomogène. On propose des équations effectives permettant de modéliser la propagation des ondes dans ce milieu. Ces équations décrivent le rôle des modes propagatifs, évanescents et radiatifs sur la propagation, et permettent de quantifier la perte radiative d'énergie dans le fond océanique. Dans un second chapitre, on s'intéresse à la propagation et à la refocalisation par retournement temporel d'une impulsion dans le modèle de guide d'onde océanique du premier chapitre. On obtient une description de l'onde refocalisée prenant en compte la perte radiative dans le fond océanique et l'évolution des fluctuations du milieu entre les deux étapes de l'expérience de retournement temporel. Dans le dernier chapitre, on s'intéresse à la refocalisation par retournement temporel dans un modèle de guide d'onde simple. On obtient un phénomène de super-résolution par l'insertion, devant la source, d'une section inhomogène à faible vitesse de propagation, c'est à dire qu'on obtient des tailles de taches focales plus concentrées qu'en milieu homogène.

L'objectif général de cette thèse est d'étudier les notions d'aléatoire et d'information algorithmiques - jusqu'ici restreints aux espaces symboliques - sur des espaces plus généraux, précisément les espaces métriques calculables, et d'appliquer ces notions à la théorie des systèmes dynamiques. Les principaux apports sont : (1) le développement d'un cadre robuste pour l'étude d'objets mathématiques (mesures de probabilité, systèmes dynamiques et leurs modèles symboliques) d'un point de vue algorithmique, notamment l'introduction et l'étude détaillée des treillis d'énumération effective; (2) l'extension de l'aléatoire algorithmique aux espaces métriques calculables, améliorant ainsi l'extension menée par Gacs qui imposait une condition supplémentaire à l'espace, et l'étude de quelques notions des probabilités classiques du point de vue de l'aléatoire; (3) un apport à la théorie des systèmes dynamiques, établissant des relations entre l'aléatoire algorithmique et l'aléatoire dynamique. Nous étudions notamment deux notions de complexité algorithmique des orbites, l'une K1 utilisant la mesure, l'autre K2 inspirée du point de vue topologique. Nous montrons que la complexité K1 des orbites partant des points aléatoires est l'entropie du système au sens de la mesure, que la borne supérieure des complexités K2 des orbites est l'entropie topologique, et que K1 et K2 coïncident pour les points aléatoires. Ce travail enrichit les résultats de Brudno et White.