L'analyse statique des programmes consiste en un ensemble de techniques permettant de déterminer des propriétés des programmes sans avoir à les exécuter. Parmi les applications de l'analyse statique des programmes, nous retrouvons l'optimisation du code source par des compilateurs et la détection de code malveillant ou de code qui pourrait être exploité à des fins malveillantes. L'évidente pertinence et l'importance (parfois critique) de telles applications expliquent les nombreuses tentatives de compréhension du cadre théorique général de l'analyse statique des programmes. Les algèbres de Kleene sont la théorie algébrique des automates finis et des expressions régulières. Cet outil algébrique s'est avéré très approprié pour l'analyse statique et la vérification des programmes. Le but de cette thèse est de développer un cadre algébrique basé sur les algèbres de Kleene pour calculer les solutions d'une classe générale de problèmes intraprocéduraux d'analyse de flot de données. Ce cadre permet de représenter les programmes, ainsi que leurs propriétés, d'une manière homogène, compacte et expressive. Les algorithmes traditionnels employés pour calculer le résultat d'une analyse sont alors remplacés par des manipulations algébriques des éléments d'une algèbre de Kleene. / L'analyse statique des programmes consiste en un ensemble de techniques permettant de déterminer des propriétés des programmes sans avoir à les exécuter. Parmi les applications de l'analyse statique des programmes, nous retrouvons l'optimisation du code source par des compilateurs et la détection de code malveillant ou de code qui pourrait être exploité à des fins malveillantes. L'évidente pertinence et l'importance (parfois critique) de telles applications expliquent les nombreuses tentatives de compréhension du cadre théorique général de l'analyse statique des programmes. Les algèbres de Kleene sont la théorie algébrique des automates finis et des expressions régulières. Cet outil algébrique s'est avéré très approprié pour l'analyse statique et la vérification des programmes. Le but de cette thèse est de développer un cadre algébrique basé sur les algèbres de Kleene pour calculer les solutions d'une classe générale de problèmes intraprocéduraux d'analyse de flot de données. Ce cadre permet de représenter les programmes, ainsi que leurs propriétés, d'une manière homogène, compacte et expressive. Les algorithmes traditionnels employés pour calculer le résultat d'une analyse sont alors remplacés par des manipulations algébriques des éléments d'une algèbre de Kleene. / Static program analysis consists of techniques for determining properties of programs without actually running them. Among the applications of static program analysis are the optimization by compilers of object code and the detection of malicious code or code that might be maliciously exploited. The obvious relevance and (sometimes critical) importance of such applications explain the many attempts to try to understand the general theoretical framework of static program analysis. Kleene algebra is the algebraic theory of finite automata and regular expressions. This algebraic tool has proven to be very suitable for the purpose of static analysis and verification of programs. The goal of this thesis is to develop an algebraic framework based on Kleene algebra to compute the solutions to a general class of intraprocedural dataflow analysis problems. The framework allows one to represent both the programs and the relevant properties in an homogeneous, compact and readable way. Traditional algorithms used to compute the result of an analysis are then replaced by algebraic manipulations of elements of a Kleene algebra. / Static program analysis consists of techniques for determining properties of programs without actually running them. Among the applications of static program analysis are the optimization by compilers of object code and the detection of malicious code or code that might be maliciously exploited. The obvious relevance and (sometimes critical) importance of such applications explain the many attempts to try to understand the general theoretical framework of static program analysis. Kleene algebra is the algebraic theory of finite automata and regular expressions. This algebraic tool has proven to be very suitable for the purpose of static analysis and verification of programs. The goal of this thesis is to develop an algebraic framework based on Kleene algebra to compute the solutions to a general class of intraprocedural dataflow analysis problems. The framework allows one to represent both the programs and the relevant properties in an homogeneous, compact and readable way. Traditional algorithms used to compute the result of an analysis are then replaced by algebraic manipulations of elements of a Kleene algebra.

Thèse numérisée 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.

Cette thèse propose un nouveau type de systèmes de ré-écriture, appelé les systèmes de réécriture fonctionnels. Nous montrons que notre modèle a la puissance d'expression des systèmes de ré-écriture et qu'il est bien adapté à l'étude de propriétés de sûreté et de propriétés de logique temporelle de modèles.Nous avons mis en évidence une sous classe de systèmes fonctionnels, les élémentaires et les élémentaires à droite, préservant la puissance d'expression des systèmes fonctionnels et des techniques d'accélération des calculs aboutissant à un outil de vérification symbolique efficace.Dans la partie expérimentale, nous avons comparé notre outil, d'une part avec des outils de ré-écriture tels que Timbuk, Maude et TOM, d'autre part avec des outils de vérification tels que SPIN, NuSMV, SMART, HSDD. Nos benchmarks démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles.

Les protocoles de sécurité sont des programmes informatiques qui définissent des règles d'échange entre les points d'un réseau et permettent de sécuriser les communications. Ils sont utilisés par exemple dans les distributeurs de billets, les abonnements aux chaînes de télévision payantes, la téléphonie mobile, le commerce électronique. Leur objectif est de garantir le secret d'une donnée, d'authentifier un des participants, de garantir l'anonymat ou la non-répudiation, etc. Ces programmes sont exécutés sur des réseaux ouverts facilement accessibles (comme internet). Aussi, pour démontrer qu'ils remplissent bien leurs objectifs, il est nécessaire de prendre en compte les attaques dont ils peuvent faire l'objet. L'objet de mon mémoire d'habilitation à diriger des recherches est de montrer que les méthodes formelles peuvent être utilisées avec succès pour entreprendre une analyse fine des protocoles cryptographiques, à travers une palette variée d'outils. Nous présentons des procédures pour déterminer de façon automatique si un protocole est sûr. Nous avons proposés différents algorithmes en fonction des propriétés de sécurité considérées ainsi que des primitives cryptographiques utilisées (chiffrement, signature, hachage, ou exclusif, etc.). D'autre part, nous caractérisons des conditions qui permettent de combiner les résultats précédents et de concevoir les protocoles de façon modulaire. Ces résultats se basent sur des modèles symboliques, très différents de ceux utilisés en cryptographie où la notion de sécurité est basée sur la théorie de la complexité. Cette notion de sécurité est mieux adaptée pour identifier toutes les attaques possibles dans la réalité mais, en contrepartie, les (lourdes) preuves de sécurité sont effectuées à la main et semblent difficilement automatisables. Nous avons identifié des hypothèses cryptographiques qui permettent de relier les approches cryptographiques et symboliques. Il est alors possible d'obtenir des preuves de sécurité à un niveau cryptographique, directement à partir des preuves établies (automatiquement) dans un cadre symbolique.

Cette thèse porte sur les mesures expérimentales des γ-prompts créés lors de la fragmentation du faisceau d'ions carbone en hadronthérapie. Deux expériences ont été effectuées aux laboratoires GANIL et GSI avec des ions 12C6+ de 95MeV/u et 305MeV/u irradiant une cible d'eau ou de PMMA. Dans les deux expériences une nette corrélation a été obtenue entre le parcours des ions carbone et le profil longitudinal des γ- prompts. Une des plus grandes difficultés de ces mesures vient de la discrimination entre le signal des γ-prompts (qui est corrélé avec le parcours des ions) et un important bruit de fond dû aux neutrons (non corrélé au parcours). Deux techniques sont employées pour effectuer la discrimination entre γ et neutrons: le temps de vol (TDV) et la discrimination par forme de signal (DFS). Le TDV a permis de démontrer la corrélation entre la production de γ-prompts et le parcours des ions. La DFS a fourni des informations précieuses pour la compréhension des caractéristiques des spectres en TDV. Dans ce travail on a démontré qu'un système de détection de γ-prompt collimaté, basé sur la technique du temps de vol, peut permettre une vérification en temps réel de la position du Pic de Bragg en conditions cliniques. Dans la dernière partie de la thèse, un travail de simulation a été effectué à l'aide du code de simulation Geant4 pour évaluer l'influence des principaux paramètres du design d'un dispositif de multi-détecteurs et multicollimateurs sur la résolution spatiale et l'efficacité atteignable par une Camera γ-Prompt. Plusieurs configurations géométriques ont été étudiées de façon systématique et les principales contraintes du design sont analysées.

Mémoire numérisé 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.

L’objectif de cette thèse est d’obtenir des algorithmes sous linéaire permettant de répondre à des problèmes de décision dans les bases de données XML. Plus précisément, on s’inspire du property testing, pour décider approximativement si un arbre d’arité non bornée est valide par rapport à une DTD ; ou plus généralement si un tel arbre est reconnu par un automate d’arbre.Nous avons d’abord étudié le cas simple des mots, c’est-à-dire l’appartenance approchée d’un mot à un langage régulier défini par un automate non-déterministe. Sous la distance d’édition entres les mots, nous proposons un algorithme (ou tester) résolvant l’appartenance approchée en un temps polynomial : en la taille de l’automate aussi bien qu’en la précision (où le paramètre d’erreur). Nous avons aussi amélioré le précédent algorithme d’Alon, Krivelevich, Newman, et Szegedy, (2000) pour l’approximation de l’appartenance à un langage régulier modulo la distance de Hamming. Notre amélioration consiste à rendre cet algorithme polynomial en la taille de l’automate non-déterministe. Ensuite nous avons considéré l’appartenance approchée d’un arbre à un automate d’arbre sous la distance d’édition standard. Notre algorithme résout ce problème avec une complexité en temps exponentielle en la hauteur de l’arbre. Enfin nous avons considéré la validation approchée de DTD par rapport à la « strong edit distance » ; et nous obtenons dans ce cas un algorithme polynomial en la hauteur de l’arbre. Nous complétons nos résultats en prouvant une borne inférieure linéaire en la taille de l’arbre, pour la complexité de tout algorithme décidant l’appartenance approchée d’un arbre à une DTD, sous la strong edit distance. / Inspired by property testing, our objective is to obtain sublinear algorithms for deciding properties of XML databases approximatively. More precisely, we investigate the properties of whether an unranked tree is valid for a DTD, or more generally, whether it is recognized by a tree automaton. We start our studies by the simpler case of words and we considered the approximate membership problem for word non-deterministic automata. For this problem, we provide an efficient tester that runs in polynomial time in the size of the input automata and the error precision. We also improve the previous [Alon, Krivelevich, Newman, and Szegedy, 2000b] approximate membership tester for regular languages modulo the Hamming distance, so that it runs in polynomial time in the size of the input automata. Secondly, we study approximate membership testing for tree automata modulo the standard edit distance, and obtain a tester with run time exponential in the input tree depth. Next we consider approximate DTD validity modulo the strong edit distance. We then provide a tester that depends polynomially on the height of the tree. Finally, modulo the strong edit distance, we prove a linear lower bound on the depth of the input tree.

Les systèmes distribués sont au coeur des technologies de l'information.Il est devenu classique de s'appuyer sur multiples unités distribuées pour améliorer la performance d'une application, la tolérance aux pannes, ou pour traiter problèmes dépassant les capacités d'une seule unité de traitement. La conception d'algorithmes adaptés au contexte distribué est particulièrement difficile en raison de l'asynchronisme et du non-déterminisme qui caractérisent ces systèmes. La simulation offre la possibilité d'étudier les performances des applications distribuées sans la complexité et le coût des plates-formes d'exécution réelles. Par ailleurs, le model checking permet d'évaluer la correction de ces systèmes de manière entièrement automatique. Dans cette thèse, nous explorons l'idée d'intégrer au sein d'un même outil un model checker et un simulateur de systèmes distribués. Nous souhaitons ainsi pouvoir évaluer la performance et la correction des applications distribuées. Pour faire face au problème de l'explosion combinatoire des états, nous présentons un algorithme de réduction dynamique par ordre partiel (DPOR), qui effectue une exploration basée sur un ensemble réduit de primitives de réseau. Cette approche permet de vérifier les programmes écrits avec n'importe laquelle des interfaces de communication proposées par le simulateur. Nous avons pour cela développé une spécification formelle complète de la sémantique de ces primitives réseau qui permet de raisonner sur l'indépendance des actions de communication nécessaire à la DPOR. Nous montrons au travers de résultats expérimentaux que notre approche est capable de traiter des programmes C non triviaux et non modifiés, écrits pour le simulateur SimGrid. Par ailleurs, nous proposons une solution au problème du passage à l'échelle des simulations limitées pour le CPU, ce qui permet d'envisager la simulation d'applications pair-à-pair comportant plusieurs millions de noeuds. Contrairement aux approches classiques de parallélisation, nous proposons une parallélisation des étapes internes de la simulation, tout en gardant l'ensemble du processus séquentiel. Nous présentons une analyse de la complexité de l'algorithme de simulation parallèle, et nous la comparons à l'algorithme classique séquentiel pour obtenir un critère qui caractérise les situations où un gain de performances peut être attendu avec notre approche. Un résultat important est l'observation de la relation entre la précision numérique des modèles utilisés pour simuler les ressources matérielles, avec le degré potentiel de parallélisation atteignables avec cette approche. Nous présentons plusieurs cas d'étude bénéficiant de la simulation parallèle, et nous détaillons les résultats d'une simulation à une échelle sans précédent du protocole pair-à-pair Chord avec deux millions de noeuds, exécutée sur une seule machine avec un modèle précis du réseau / Distributed systems are in the mainstream of information technology. It has become standard to rely on multiple distributed units to improve the performance of the application, help tolerate component failures, or handle problems too large to fit in a single processing unit. The design of algorithms adapted to the distributed context is particularly difficult due to the asynchrony and the nondeterminism that characterize distributed systems. Simulation offers the ability to study the performance of distributed applications without the complexity and cost of the real execution platforms. On the other hand, model checking allows to assess the correctness of such systems in a fully automatic manner. In this thesis, we explore the idea of integrating a model checker with a simulator for distributed systems in a single framework to gain performance and correctness assessment capabilities. To deal with the state explosion problem, we present a dynamic partial order reduction algorithm that performs the exploration based on a reduced set of networking primitives, that allows to verify programs written for any of the communication APIs offered by the simulator. This is only possible after the development of a full formal specification with the semantics of these networking primitives, that allows to reason about the independency of the communication actions as required by the DPOR algorithm. We show through experimental results that our approach is capable of dealing with non trivial unmodified C programs written for the SimGrid simulator. Moreover, we propose a solution to the problem of scalability for CPU bound simulations, envisioning the simulation of Peer-to-Peer applications with millions of participating nodes. Contrary to classical parallelization approaches, we propose parallelizing some internal steps of the simulation, while keeping the whole process sequential. We present a complexity analysis of the simulation algorithm, and we compare it to the classical sequential algorithm to obtain a criteria that describes in what situations a speed up can be expected. An important result is the observation of the relation between the precision of the models used to simulate the hardware resources, and the potential degree of parallelization attainable with this approach. We present several case studies that benefit from the parallel simulation, and we show the results of a simulation at unprecedented scale of the Chord Peer-to-Peer protocol with two millions nodes executed in a single machine