Enjeu majeur de santé publique, les maladies chroniques nécessitent souvent une approche multidisciplinaire et des contacts multiples entre le patient et le système de soins. La maîtrise de ce parcours, la trajectoire de soins, est un gage de qualité des soins, qualité de vie et d'efficience médico-économique. Pour maîtriser les trajectoires de soins, il faut les connaître. Or, à ce jour en France, aucun système d'information en santé à grande échelle n'est conçu pour décrire les trajectoires de soins, encore moins d'en établir une typologie. Malgré tout, d'énormes quantités de données sont produites chaque année par le système de soins. Dans ce travail, nous proposons un système d'analyse et de représentation des trajectoires de soins à partir de données récoltées à l'origine pour d'autres utilisations. Ce système est fondé sur l'Analyse Formelle de Concepts (AFC), une méthode de classification conceptuelle capable de découvrir des liens naturels dans les données d'un tableau binaire et de les représenter sous forme de treillis de concepts. Nous montrons les apports de l'AFC dans la compréhension du fonctionnement du système de soins et les perspectives en termes d'exploration des réseaux sociaux en général. Par ailleurs, nous étudions, combinons et comparons deux mesures d'intérêt pour réduire la complexité des grands treillis et sélectionner les connaissances les plus pertinentes : la stabilité et le support d'un concept. Dans un parallèle avec la recherche de motifs fréquents simple et séquentiels, nous proposons une méthode de classification non supervisée des trajectoires de soins qui présente d'intéressantes capacités de visualisation et d'interprétabilité.

Les systèmes temps réel et distribués posent des problèmes complexes en termes de conception d'architecture et de description de comportements. De par leur criticité en vies humaines et leurs coûts de prototypage, ces systèmes ont motivé le développement d'une activité de recherche sur les langages de modélisation formelle et les techniques de validation basées modèle qui contribuent à la détection au plus tôt des erreurs de conception. Néanmoins, les langages formels ont eu un succès plus que limité dans l'industrie. L'arrivée du langage UML (Unified Modeling Language) a ouvert de nouveaux horizons pour l'intégration de langages de modélisation formelle dans une méthodologie de conception susceptible d'être mieux acceptée par les praticiens du domaine. En s'appuyant sur une expérience antérieure de la technique de description formelle Estelle et des extensions temporelles des réseaux de Petri, notre activité de recherche sur les cinq dernières années a débouché sur la production d'un profil UML nommé TURTLE (Timed UML and RT-LOTOS Environment). TURTLE surpasse UML 2.0 par ses extensions aux diagrammes d'analyse et de conception UML, sa sémantique formelle exprimée en RT-LOTOS, et ses outils de support (éditeur de diagrammes et outil de validation formelle combinant simulation et vérification basée sur une analyse daccessibilité). La méthodologie TURTLE trouve son champ d'application naturel dans la conception de systèmes temps réel et la validation d'architectures de communication en particulier. L'approche proposée a été appliquée avec succès à des systèmes satellitaires et des protocoles d'authentification.

Une carte est le plongement d'un graphe dans une surface, à un homéomorphisme près. Ainsi, une carte est un objet topologique énumérable, en fonction du nombre de ses sommets, de ses arêtes et de ses faces. Les cartes admettent des symétries internes qui rendent leur énumération difficile. On n'envisage dans ce travail que l'énumération des cartes pointées, le pointage supprimant toutes les symétries. Le nombre exact de cartes pointées sur une surface donnée n'est connu que pour les surfaces de petit genre, comme la sphère (genre 0), le tore ou le plan projectif (genre 1). En effet, la complexité des méthodes de calcul de ces nombres augmente rapidement avec le genre des surfaces. Un travail important de cette thèse a été de convertir l'une de ces méthodes de calcul en une preuve de l'existence d'une structure commune à toutes les séries génératrices de cartes pointées de genre non nul. Pour chaque surface orientable, on réduit le problème à la détermination d'un polynôme, dont le degré est majoré par une fonction simple du genre de la surface. Un résultat analogue est obtenu pour les cartes pointées sur les surfaces non orientables. Des conséquences pratiques et une implantation logicielle de tous ces résultats sont décrites. De nouvelles formules explicites d'énumération sont données. Indépendamment, une bijection géométrique nouvelle est exposée, entre certaines cartes 2-coloriables et les partitions de polygones, énumérées par les nombres de Schröder.

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

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

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

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

Plusieurs outils ont été développé pour vérifier automatiquement les propriétés de sécurité sur des protocoles cryptographiques. Jusqu'à maintenant, la plupart de ces outils permettent de vérifier des propriétés de trace (ou propriétés d'accessibilité) tel que le secret simple ou l'authentification. Néanmoins, plusieurs propriétés de sécurité ne peuvent pas être exprimés en tant que propriété de trace, mais peuvent l'être en tant que propriété d'équivalence. L'anonymat, la non-tracabilité ou le secret fort sont des exemples classique de propriété d'équivalence. Typiquement, deux protocoles P et Q sont équivalent si les actions d'un adversaire (intrus) ne lui permettent pas de distinguer P de Q. Dans la littérature, plusieurs notions d'équivalence ont été étudiés, par exemple l'équivalence de trace ou l'équivalence observationnelle. Néanmoins, ces équivalences se relèvent être très difficiles à démontrer , d'où l'importance de développer des outils de vérification automatique efficaces de ces équivalences. Au sein de cette thèse, nous avons dans un premier temps travaillé sur une approche reposant sur des techniques de résolution de contraintes et nous avons créé un nouvel algorithme pour décider l'équivalence de trace entre deux protocoles pouvant contenir des conditionnelles avec branches "else", et pouvant également être non-déterministe. Cet algorithme a été appliqué sur des exemples concrets comme le "Private authentification protocol" ainsi que le "E-passport protocol". Cette thèse propose également des résultats de composition pour l'équivalence de trace. En particulier, nous nous sommes intéressé à la composition parallèle de protocoles partageant certains secrets. Ainsi dans cette thèse, nous avons démontré que, sous certaines conditions, la composition parallèle de protocoles préserve les propriétés d'équivalence. Ce résultat fut appliqué au "E-passport protocol". Enfin, cette thèse présente une extension à l'outil de vérification automatique ProVerif afin de démontrer automatiquement plus de propriétés d'équivalence. Cette extension a été implémenté au sein de ProVerif ce qui a permis de démontrer la propriété d'anonymat pour le "Private authentification protocol" . / Many tools have been developed to automatically verify security properties on cryptographic protocols. But until recently, most tools focused on trace properties (or reachability properties) such as authentication and secrecy. However, many security properties cannot be expressed as trace properties, but can be written as equivalence properties. Privacy, unlinkability, and strong secrecy are typical examples of equivalence properties. Intuitively, two protocols P, Q are equivalent if an adversary can not distinguish P from Q by interacting with these processes. In the literature, several notions of equivalence were studied, e.g. trace equivalence or a stronger one, observational equivalence. However, it is often very difficult to prove by hand any of these equivalences, hence the need for efficient and automatic tools. We first worked on an approach that rely on constraint solving techniques and that is well suited for bounded number of sessions. We provided a new algorithm for deciding the trace equivalence between processes that may contain negative tests and non-determinism. We applied our results on concrete examples such as anonymity of the Private Authentication protocol and the E-passport protocol. We also investigated composition results. More precisely, we focused on parallel composition under shared secrets. We showed that under certain conditions on the protocols, the privacy type properties are preserved under parallel composition and under shared secrets. We applied our result on the e-passport protocol. At last this work presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. This extension have been implemented in ProVerif and allows us to automatically prove anonymity in the private authentication protocol.

On présente une Logique Probabiliste avec des opérateurs Conditionnels - LPCP, sa syntaxe, sémantique, axiomatisation correcte et fortement complète, comprenant une règle de déduction infinitaire. On prouve que LPCP est décidable, et on l'étend pour qu’il puisse représenter l'évidence, en créant ainsi la première axiomatisation propositionnelle du raisonnement basé sur l'évidence. On codifie les Logiques Probabilistes LPP1Q et LPPQ2 dans l'Assistant de Preuve Coq, et on vérifie formellement leurs propriétés principales: correction, complétude fort et non-compacité. Les deux logiques étendent la Logique Classique avec des opérateurs de probabilité, et présentent une règle de déduction infinitaire. LPPQ1 permet des itérations des opérateurs de probabilité, lorsque LPPQ2 ne le permet pas. On a formellement justifié l'utilisation des solveurs SAT probabilistes pour vérifier les questions liées à la cohérence. On présente LFP, un Cadre Logique avec Prédicats Externes, en introduisant un mécanisme pour bloquer et débloquer types et termes dans LF, en permettant l'utilisation d’oracles externes. On démontre que LFP satisfait tous les principales propriétés et on développe un cadre canonique correspondant, qui permet de prouver l’adéquation. On fournit diverses encodages - le λ-calcul non-typé avec la stratégie de réduction CBV, Programmation-par-Contrats, un langage impératif avec la Logique de Hoare, des Logiques Modales et la Logique Linéaire Non-Commutative, en montrant que en LFP on peut codifier aisément des side-conditions dans l'application des règles de typage et atteindre une séparation entre vérification et computation, en obtenant des preuves plus claires et lisibles. / We introduce a Probability Logic with Conditional Operators - LPCP, its syntax, semantics, and a sound and strongly-complete axiomatic system, featuring an infinitary inference rule. We prove the obtained formalism decidable, and extend it so as to represent evidence, making it the first propositional axiomatisation of reasoning about evidence. We encode Probability Logics LPP1Q and LPP2Q in the Proof Assistant Coq and formally verify their key properties - soundness, strong completeness, and non-compactness. Both logics extend Classical Logic with modal-like probability operators, and both feature an infinitary inference rule. LPP1Q allows iterations of probability operators, while LPP2Q does not. In this way, we have formally justified the use of Probabilistic SAT-solvers for the checking of consistency-related questions. We present LFP - a Logical Framework with External Predicates, by introducing a mechanism for locking and unlocking types and terms into LF, allowing the use of external oracles. We prove that LFP satisfies all the main meta-theoretic properties and develop a corresponding canonical framework, allowing for easy proofs of adequacy. We provide a number of encodings - the simple untyped λ-calculus with a Call-by-Value reduction strategy, the Design-by-Contract paradigm, a small imperative language with Hoare Logic, Modal Logics in Hilbert and Natural Deduction style, and Non-Commutative Linear Logic (encoded for the first time in an LF-like framework), illustrating that in LFP we can encode side-conditions on the application of rules elegantly, and achieve a separation between verification and computation, resulting in cleaner and more readable proofs.