Depuis plusieurs années, le marché des circuits intégrés numériques requiert des systèmes de plus en plus complexes dans un temps toujours plus réduit. Afin de répondre à ses deux exigences, les industriels de la conception font appel à des fournisseurs externes proposant des circuits fonctionnant sur des signaux d'horloge dédiés. Lorsque ces derniers communiquent entre eux, les horloges d'émission et de réception ne sont pas les mêmes, on parle de « Clock Domain Crossing » (CDC).Les CDC correspondent à des communications asynchrones et peuvent provoquer des dysfonctionnements critiques. Par ailleurs, ces problèmes étant intermittents et complexes à analyser, ils ne peuvent pas être exhaustivement vérifiés avec des méthodes telles que l’analyse de timing ou la simulation fonctionnelle. Avec l'augmentation du nombre de CDC dans les circuits, les industriels de la conception assistée par ordinateur (EDA) ont proposé des solutions logicielles spécialisées dans la vérification statique des CDC. Cependant, les circuits développés étant en constante évolution, les outils ne sont pas en mesure de s’adapter. Pour pallier ces problèmes, la vérification industrielle des CDC est basée sur la spécification de contraintes et d'exclusions par l'utilisateur. Ces actions, qui se substituent aux outils, peuvent masquer des bugs. De plus, l’effort humain requis par cette approche n’est pas compatible avec le temps alloué au développement de circuits industriels. Nous avons donc cherché à automatiser la vérification en proposant des solutions basées sur des propriétés formelles. Les travaux ont consisté à analyser les différentes techniques de conception et de vérification des CDC à travers l’évaluation des principaux outils du marché. A partir des résultats obtenus, nous avons formalisé les problèmes pratiques et proposé des modèles permettant d’obtenir des résultats exhaustifs automatiquement. Les essais ont été réalisés sur un sous-système à base de processeurs (CPUSS) développé chez STMicroelectronics. L'adoption de nos modèles permet une vérification complète des CPUSS de manière automatique ce qui est essentiel dans un environnement industriel compétitif. En effet, le nombre d’informations devant être spécifiées par l’utilisateur a été réduit de moitié pour chacun des outils évalués. Par ailleurs, ces travaux ont montré que l’axe de développement des outils CDC avec l’ajout de fonctionnalités telles que les flots hiérarchiques ou l’injection de fautes n’améliore pas la qualité de résultats. Une collaboration ayant été mise en place avec les principaux fournisseurs outils, certaines solutions seront probablement intégrées aux outils dans les années à venir. / For several years now, the digital IC market has been requiring both more complex systems and reduced production times. In this context, the semiconductor chip maker companies call on external IP providers offering components working on dedicated clock signals. When these IPs communicate between them, the source and destination clocks are not the same, we talk about "Clock Domain Crossing" (CDC).CDC correspond to asynchronous communications and can cause critical failures. Furthermore, due to the complexity and the random nature of CDC issues, they can not be exhaustively checked with methods such as timing analysis or functional simulation. With the increase of CDC in the digital designs, EDA tools providers have developed software solutions dedicated to CDC static verification.Whereas, the designs are subject to continuous change, the verification tools are not able to be up to date. To resolve these practical issues, the CDC industrial verification is based on the specification of constraints and exclusions by the user. This manual flow, which replaces the tools, can mask bugs. Moreover, the human effort required by this approach is incompatible with the time allowed to industrial designs development.Our goal has been to automate the verification submitting solutions based on formal properties.The work consisted in the analysis of the different CDC design and verification approaches through the evaluation of main CDC checker tools. From the results obtained, we have formalized the practical problems and proposed models to obtain automatically exhaustive results. The tests have been performed on a processor-based subsystem (CPUSS) developed at STMicroelectronics.Adopting our models enables a complete checking of CPUSS in an automatic way, which is essential within a competitive industrial environment. Actually, the amount of information to be specified by the user has been reduced by half for each one of the evaluated tools. Otherwise, this work has shown that the development axis of the CDC tools despite the addition of functionalities such as hierarchical flows or fault injection, doesn’t improve the quality of results (QoR). Since a collaboration has been established with the main tool providers some solutions would probably be included into the tools over the coming years.

Les protéines sont des macromolécules participant à d’importants processus biophysiques de la vie des organismes. Or, il a été démontré que des variations de leur structure peuvent conduire à des changements de fonction en lien avec certaines maladies telles que celles associées à des processus neurodégénératifs. Ainsi, tant pour la communauté scientifique que pour l’industrie médicale, il est capital d’avoir une meilleure compréhension de la structure de ces protéines, ainsi que de leurs interactions avec d’autres molécules, ce en vue d’inventer et d’évaluer de nouveaux médicaments.Au cours de ces travaux de thèse, nous nous sommes particulièrement intéressés au développement de nouvelles méthodes de recherche de chemins biologiquement faisables entre deux états connus pour un système composé d’une protéine ou d’une protéine et d’un ligand. Au cours des dernières décennies, une grande quantité d’approches algorithmiques ont été proposées pour faire face à ce problème. Pourtant, les méthodes développées sont encore aujourd’hui confrontées à deux grands défis : d’une part la haute dimension des espaces de recherche, associée au grand nombre d’atomes impliqués, d’autre part la complexité des interactions entre ces atomes.Cette dissertation propose deux nouvelles méthodes pour obtenir de manière efficace des chemins pertinents pour des systèmes moléculaires. Ces méthodes sont rapides et génèrent des solutions qui peuvent ensuite être analysées ou améliorées à l’aide de méthodes d’avantage spécialisées. La première approche proposée produit des chemins d’interpolation pour systèmes biomoléculaires, à l’aide des approches dites aussi-rigides-que-possible, (ARAP) utilisées en animation graphique. Cette méthode est robuste et génère des solutions préservant au mieux la rigidité du système d’origine. Une extension de cette méthode basée sur des critères énergétiques a également été proposée et s’est avérée capable d’améliorer de manière significative les chemins solution. Cependant, pour les scénarios nécessitant de complexes déformations, cette approche géométrique peut conduire à des chemins solution non naturels. Nous avons donc proposé une seconde méthode appelée ART-RRT, qui utilise l’approche ARAP pour réduire la dimensionalité de l’espace et la combine avec les arbres d’exploration RRT (Rapidely-exploring Random Tree) issus de la Robotique, afin d’explorer efficacement les chemins possibles de l’espace.En plus de fournir une variété de solutions en temps raisonnable, cette ART-RRT produit des chemins de faible énergie, sans collision et dont la rigidité est préservée autant que possible. Des versions monodirectionnelles de bidirectionelles de cette méthode ont été proposées et appliquées respectivement à la recherche de chemin d’extraction d’un ligand hors du site actif d’une protéine, ainsi qu’a la recherche de chemin de transition conformationnelle pour protéine seule. Les solutions trouvées se sont avérées être en accord avec les données expérimentales ainsi qu’avec les solutions issues de l’état de l’art. / Proteins are macromolecules participating in important biophysical processes of living organisms. It has been shown that changes in protein structures can lead to changes in their functions and are found linked to some diseases such as those related to neurodegenerative processes. Hence, an understanding of their structures and interactions with other molecules such as ligands is of major concern for the scientific community and the medical industry for inventing and assessing new drugs.In this dissertation, we are particularly interested in developing new methods to find for a system made of a single protein or a protein and a ligand, the pathways that allow changing from one state to another. During past decade, a vast amount of computational methods has been proposed to address this problem. However, these methods still have to face two challenges: the high dimensionality of the representation space, associated to the large number of atoms in these systems, and the complexity of the interactions between these atoms.This dissertation proposes two novel methods to efficiently find relevant pathways for such biomolecular systems. The methods are fast and their solutions can be used, analyzed or improved with more specialized methods. The first proposed method generates interpolation pathways for biomolecular systems using the As-Rigid-As-Possible (ARAP) principle from Computer Graphics. The method is robust and the generated solutions preserve at best the local rigidity of the original system. An energy-based extension of the method is also proposed, which significantly improves the solution paths. However, in scenarios requiring complex deformations, this geometric approach may still generate unnatural paths. Therefore, we propose a second method called ART-RRT, which combines the ARAP principle for reducing the dimensionality, with the Rapidly-exploring Random Trees from Robotics for efficiently exploring possible pathways. This method not only gives a variety of pathways in reasonable time but the pathways are also low-energy and clash-free, with the local rigidity preserved as much as possible. The mono-directional and bi-directional versions of the ART-RRT method were applied for finding ligand-unbinding and protein conformational transition pathways, respectively. The results are found to be in good agreement with experimental data and other state-of-the-art solutions.

Cette thèse porte sur la circulation de la théâtralité du cirque, de la France aux régions intérieures du Brésil, en prenant comme référence la configuration du spectacle de cirque moderne et la présence du théâtre dans le Cirque Olympique de 1807 à 1836. Le théâtre y est considéré comme un des éléments de la pluralité du cirque qui arriva au Brésil au XIXe siècle. Pour comprendre la circulation de cette dramaturgie, l’étude se porte sur le système de transports du pays, en se focalisant sur les chemins de fer, afin de mesurer l’impact culturel du Bahia and São Francisco Railway et du Chemin de Fer São Francisco dans les régions intérieures de l’Etat de Bahia, pendant la première moitié du XXe siècle. Ce qui permet de réaliser une analyse de la vie culturelle de ce « réseau de villes » bénéficiaires des chemins de fer, en particulier les villes de Alagoinhas, Serrinha, Senhor do Bonfim et Juazeiro. A titre d’exemple de cette circulation, l’étude se concentre sur le mélodrame français Les deux sergents, de D’Aubigny, présenté pour la première fois au public au Théâtre de la Porte Saint-Martin en 1823. Traduit en portugais, il fut représenté par des cirques et des compagnies théâtrales, dans différentes villes du Brésil, dont celles étudiées ici, et illustre un vrai triomphe de la dramaturgie mélodramatique française au Brésil, pendant plus d’un siècle. / This paper discusses the transit of the circus-theatricality from France to the interior of Brazil with reference to the configuration of the modern circus show and the presence of the theatre at the Cirque Olympique between the years 1807 and 1836. The theatre is therefore treated as an element of the plurality of the circus that came to Brazil in the nineteenth century. To understanding this circulation it is necessary to analyse the transport system in the country, focusing on the railroads, to point out the cultural impacts of the Bahia and San Francisco Railway and the Railway San Francisco on the interior of Bahia in the first half of the twentieth century and an analysis of the cultural life in the "network of cities" in Bahia, benefited by the railroads, especially the cities Alagoinhas, Serrinha, Senhor do Bonfim and Juazeiro. As an example of this movement, we discuss the French melodrama Les deux sergents from D'Aubigny, whose debut performance took place at the Théâtre de la Porte Saint-Martin in 1823. Translated into Portuguese, the piece was performed by circuses and theatre companies in several Brazilian cities, including those encompassed by this study, featuring a triumph of French melodramatic dramaturgy in Brazil over the course of more than a century.

La croissance rapide dans le domaine des semi-conducteurs fait que les circuits digitaux deviennent de plus en plus complexes. La capacité à identifier la cause réelle d'une défaillance dans un circuit digital est donc critique. Le diagnostic logique est une procédure qui permet de localiser une erreur observée dans un circuit fautif, l'analyse de défaillance peut être ensuite appliquée pour déterminer la cause réelle de cette erreur. Un diagnostic efficace et précis est donc fondamental pour améliorer les résultats de l'analyse de défaillance et augmenter éventuellement le rendement de production."Effet à Cause" et "Cause à Effet" sont deux approches classiques pour le diagnostic logique. Ce diagnostic fournit une liste de suspects au niveau porte logique. Cependant, cette approche n'est pas précise dans le cas où le défaut est localisé à l'intérieur de la cellule logique.Dans cette thèse, nous proposons une nouvelle méthode de diagnostic intra-cell basé sur l'approche "Effet à Cause" pour améliorer la précision de la localisation de défaut au niveau transistor. L'approche proposée utilise l'algorithme CPT (Traçage de chemins critiques) appliqué au niveau transistor. Pour chaque cellule suspecte, nous appliquons un CPT avec les vecteurs de test fautifs. Le résultat obtenu est une liste de suspects préliminaires. Chaque suspect peut être un noeud (G, S, D) de transistor. Par la suite, nous appliquons un CPT avec les vecteurs de test non-fautifs pour minimiser la liste de suspects. La méthode proposée donne la localisation précise du défaut pour une erreur observée. Par ailleurs, la méthode est indépendante du modèle de faute invoqué. / The rapid growth in semiconductor field results in an increasing complexity of digital circuits. The ability to identify the root cause of a failing digital circuit is becoming critical for defect localization. Logic diagnosis is the process of isolating the source of observed errors in a defective circuit, so that a physical failure analysis can be performed to determine the root cause of such errors. Effective and precise logic diagnosis is crucial to speed up the failure analysis and eventually to improve the yield.“Effect-Cause” and “Cause-Effect” are the two classical approaches for logic diagnosis. Logic diagnosis provides a list of gates as suspects. However, this approach may not leads to accurate results in the case of the defect is inside a gate.We propose a new intra-cell diagnosis method based on “Effect-Cause” approach to improve the defect localization accuracy at transistor level. The proposed approach exploits the CPT (Critical Path Tracing) applied at transistor level. For each suspected cell, we apply the CPT for every given failing test vector. The result is a preliminary list of candidates. Each candidate can be a net or a transistor drain, gate or source. After that, we apply the CPT for each passing test vector in order to narrow down the the list of candidates. The proposed method gives precise localization of the root cause of the observed errors. Moreover, it does not require the explicit use of a fault model.

Réformes des chemins de fer en Europe : la régulation en complément des mécanismes de marché Afin de trouver un nouveau dynamisme, l’Europe des chemins de fer a entrepris d’importants changements visant in fine à introduire une pression concurrentielle dans un secteur précédemment dominé par des monopoles étatiques.A l'instar des changements ayant eu lieu dans les autres industries de réseaux, la gestion en amont des infrastructures - considérée comme un monopole naturel - a été séparée du marché aval des services ferroviaires, considéré lui comme contestable, c’est-à-dire propice à l’introduction de la concurrence.Néanmoins l’expérience de réformes similaires nous rappelle que les marchés découlant d’une telle réorganisation doivent être manufacturés et ne se forment pas spontanément.Dans cette thèse, nous capitalisons sur cette période de changements afin d’analyser comment une telle transition se réalise. Plus spécifiquement, en appliquant le cadre développé par la Théorie de la Firme, les défis liés à la séparation verticale et au besoin de coordination sont examinés. Puis en s’appuyant sur les outils de la Théorie de l’Agence, nous étudions les implications dé-13coulant de l’introduction d’appels d’offres dans la délégation de service public pour le transport régional de voyageur. Au long de la thèse, l’accent est mis sur le rôle de la régulation et sur les remèdes qu’elle peut offrir aux écueils rencontrés.Le chapitre 1 analyse comment les réformes ont été conçues à travers l’Europe.Car en pratique la mise en oeuvre de cette nouvelle stratégie ferroviaire varie grandement d’un pays à l’autre à plusieurs niveaux, tels que la structure verticale,la régulation ou encore la libéralisation du secteur aval, engendrant d’importants débats sur les mérites respectifs de chacune de ces options. Cette pluralité interroge également sur les motivations sous-jacentes à chacun de ces choix. Et bien que la littérature économique aborde ces motivations, les études empiriques précédentes ne les prennent pas en compte quand il s’agit de comparer les différentes formes verticales. De ce fait, l’endogénéité peut venir biaiser les résultats des estimations économétriques. Ayant construit une base de données couvrant les quatre années entre 2009 et 2012 pour 25 pays européens, nous appliquons la méthode des doubles moindres carrées (2SLS)pour obtenir une estimation non-biaisée des effets de chacune des dimensions précédemment évoquées. En particulier, nous trouvons que l’endogénéité crée effectivement un biais qui péjore les effets mesurés de la séparation verticale.Le chapitre 2 s'appuie sur le cas du secteur ferroviaire français pour illustrer une des répercussions souvent sous-estimées de la séparation verticale, celle des coûts de coordination. Nous développons un modèle expliquant pourquoi la coordination peut aboutir à des résultats inefficients dans un secteur ferroviaire où les firmes doivent s'engager ex ante sur les quantités. Nos résultats indiquent qu’une régulation crédible peut permettre de surmonter les limites de la séparation verticale pour le gestionnaire d’infrastructure. Cependant dans un marché qui n’est pas suffisamment flexible, il devient plus dur au fur et à mesure que le marché aval s’ouvre à la concurrence de soutenir une production importante. / In an objective to revitalize the sector, railways in Europe have gone through changes in order to introduce competitive forces in an industry previous lydominated by state monopolies. Not unlike what occurred in other network industries, the upstream management of infrastructure -considered a natural monopoly- was separated from the downstream market of train services which was deemed contestable. But the experience from previous reforms shows that the markets stemming from this new organisation are made and don’t necessarily just happen.This dissertation preys on those changing times to analyse how such transition can be achieved. More specifically, it uses the framework developed by the Theory of the Firm to investigate some of the challenges that have risen to investigate some of the challenges that have risen from this new organisation due to vertical separation and the need to develop coordination. Then using the tools developed by Agency Theory, the dissertation investigates the introduction of tendering in public procurement for rail services.Throughout the analysis, an emphasis is put on finding how regulation can provide a remedy to the identified challenges. In chapter 1, we review how the reforms were designed in Europe. It highlights that there was very various applications across countries on several dimensions such as the vertical structure, regulation or downstream competition, triggering debates on the relative merits of each option.relative merits of each option.Furthermore this plurality questions the motivations behind these choices. And although those motivationsare brought up in the literature, the previous empirical studies do nottake them into account when comparing the relative performance of one form against the other. In such a case, endogeneity might come and biased the results of econometric regressions. Having constructed a database covering four years between 2009 and 2012 in 25 European countries we use a two-stageleast-square model to obtain an unbiased estimate of the effects of the abovementioned dimensions. In conclusion, we find that endogeneity does create abias, in particular when measuring the merits of full separation. Chapter 2 builds on the French rail sector’s example to shed the light on the crucial and understudied impact of coordination costs, one of the drawbacks arising with separation in the sector. We develop a model explaining why inefficient outcomes may arise in the railway sector when vertically separated firms have to commit ex ante on quantities. Our results indicate that credible and effective price regulation can overcome the limits of separation on the infrastructure side. On the other hand, if the market is not flexible enough, it may become harder, as the downstream market is becoming more competitive, for train operators to make optimistic production forecasts.

La construction et l'exploitation de la ligne Haiphong-Yunnan avaient lieu dans le cadre de la présentation française au Viet Nam, débutée en1858 par l'attaque du port de Tourane (Đà Nẵng) et interrompue en 1945, après le coup de force japonais et la déclaration de l'indépendance du Vietnam. En réalité, les processus de construction et d'exploitation de cette ligne avaient une influence sur la société et sur l'économie du Tonkin dans la période coloniale. L'objectif de cette thèse donc consiste à examiner ces influences socio-économiques et sociopolitiques de ce chemin de fer. De plus, la thèse vise également 1) à la vie des travailleurs sur les chantiers de construction dans la haute région du Tonkin, 2) à la rentabilité de la Compagnie des chemins de fer de l'Indochine et du Yunnan et 3) au rôle de cette ligne dans la Deuxième Guerre Mondiale. / The construction and the operation of the Haiphong-Yunnan railway took place in the framework of the French presentation in Viet Nam, started by the attack in 1858 at the port Tourane (Da Nang) and suspended in 1945, after the Japanese coup and the declaration of the independence of Vietnam. In fact, the process of construction and operation of this line had an influence on the society and the economy of Tonkin. The objective of this thesis is to examine the socio-economic and socio-political influences of this railway. In addition, the thesis also aims 1) to the lives of workers on construction sites in the Upper-Tonkin, 2) the profitability of the Company railways Indochina and Yunnan and 3) the role of this line throughout the Second World War.

Le but de cette thèse est d'établir des résultats énumératifs sur certaines classes de chemins et d'animaux. Ces résultats sont obtenus en appliquant la théorie des empilements de pièces développée par Viennot. Nous étudions les excursions discrètes (ou chemins de Dyck généralisés) de hauteur bornée; nous obtenons des résultats énumératifs qui interprètent combinatoirement et étendent des résultats de Banderier, Flajolet et Bousquet-Mélou. Nous décrivons et énumérons plusieurs classes de chemins auto-évitants, dits chemins faiblement dirigés. Ces chemins sont plus nombreux que les chemins prudents qui forment la classe naturelle la plus grande jusqu'alors. Nous calculons le périmètre de site moyen des animaux dirigés, prouvant des conjectures de Conway et Le Borgne. Enfin, nous obtenons des résultats nouveaux sur l'énumération des animaux de Klarner et les animaux multi-dirigés de Bousquet-Mélou et Rechnitzer. / The goal of this thesis is to prove enumerative results on some classes of lattice walks and animals. These results are applications of the theory of heaps of pieces developed by Viennot. We study discrete excursions (or generalized Dyck paths) with bounded height; we obtain enumerative results that give a combinatorial interpretation and extend results by Banderier, Flajolet and Bousquet-Mélou. We describe and enumerate several classes of self-avoiding walks called weakly directed walks. These classes are larger than the class of prudent walks, the largest natural class enumerated so far. We compute the average site perimeter of directed animals, proving conjectures by Conway and Le Borgne. Finally, we obtain new results on the enumeration of Klarner animals and multi-directed animals defined by Bousquet-Mélou and Rechnitzer.

Le test boîte blanche basé sur les chemins est largement utilisé pour la validation de programmes. A partir du graphe de flot de contrôle (CFG) du programme sous test, les cas de test sont générés en sélectionnant des chemins d'intérêt, puis en essayant de fournir, pour chaque chemin, des valeurs d'entrées concrètes qui déclencheront l'exécution du programme le long de ce chemin.Il existe de nombreuses manières de définir les chemins d'intérêt: les méthodes de test structurel sélectionnent des chemins remplissant un critère de couverture concernant les éléments du graphe; dans l'approche aléatoire, les chemins sont tirés selon une distribution de probabilité sur ces éléments. Ces méthodes aléatoires ont l'avantage de fournir un moyen d'évaluer la qualité d'un jeu de test à travers la probabilité minimale de couvrir un élément du critère.Fournir des valeurs concrètes d'entrées nécessite de construire le prédicat de cheminement chaque chemin, i.e. la conjonction des contraintes sur les entrées devant être vérifiée pour que le système s'exécute le long de ce chemin. Cette construction se fait par exécution symbolique. Les données de test sont ensuite déterminées par résolution de contraintes. Si le prédicat d'un chemin est insatisfiable, le chemin est dit infaisable. Il est très courant qu'un programme présente de tels chemins, leur nombre surpassent généralement de loin celui des faisables. Les chemins infaisables sélectionnés lors la première étape ne contribuent pas au jeu de test final, et doivent être tirés à nouveau. La présence de ces chemins pose un sérieux problème aux méthodes structurelles et à toutes les méthodes d'analyse statique, la qualité des approximations qu'elles fournissent étant réduite par les données calculées le long de chemins infaisables.De nombreuses méthodes ont été proposées pour résoudre ce problème, telles que le test concolique ou le test aléatoire basé sur les domaines d'entrée. Nous présentons un algorithme qui construit de meilleures approximations du comportement d'un programme que son CFG, produisant un nouveau CFG qui sur-approxime l'ensemble des chemins faisables mais présentant moins de chemins infaisables. C'est dans ce nouveau graphe que sont tirés les chemins.Nous avons modélisé notre approche et prouvé formellement, à l'aide de l'assistant de preuve interactif Isabelle/HOL, les propriétés principales établissant sa correction.Notre algorithme se base sur l'exécution symbolique et la résolution de contraintes, permettant de détecter si certains chemins sont infaisables ou non. Nos programmes peuvent contenir des boucles, et leurs graphes des cycles. Afin d'éviter de suivre infiniment les chemins cycliques, nous étendons l'exécution symbolique avec la détection de subsomptions. Une subsomption peut être vue comme le fait qu'un certain point atteint durant l'analyse est un cas particulier d'un autre atteint précédemment: il n'est pas nécessaire d'explorer les successeurs d'un point subsumé, ils sont subsumés par les successeurs du subsumeur. Notre algorithme a été implémenté par un prototype, dont la conception suit fidèlement la formalisation, offrant un haut niveau de confiance dans sa correction.Dans cette thèse, nous présentons les concepts théoriques sur lesquels notre approche se base, sa formalisation à l'aide d'Isabelle/HOL, les algorithmes implémentés par notre prototype et les diverses expériences menées et résultats obtenus à l'aide de ce prototype. / White-box, path-based, testing is largely used for the validation of programs. Given the control-flow graph (CFG) of the program under test, a test suit is generated by selecting a collection of paths of interest, then trying to provide, for each path, some concrete input values that will make the program follow that path during a run.For the first step, there are various ways to define paths of interest: structural testing methods select some set of paths that fulfills coverage criteria related to elements of the graph; in random-based techniques, paths are selected according to a given distribution of probability over these elements (for instance, uniform probability over all paths of length less than a given bound). Both approaches can be combined as in structural statistical testing. The random-based methods above have the advantage of providing a way to assess the quality of a test set as the minimal probability of covering an element of a criterion.The second step requires to produce for each path its path predicate, i.e. the conjunction of the constraints over the input parameters that must hold for the system to run along that path. This is done using symbolic execution. Then, constraint-solving is used to compute test data. If there is no input values such that the path predicate evaluates to true, the path is infeasible. It is very common for a program to have infeasible paths and such paths can largely outnumber feasible paths. Infeasible paths selected during the first step will not contribute to the final test suite, and there is no better choice than to select another path, hoping for its feasibility. Handling infeasible paths is the serious limitation of structural methods since most of the time is spent selecting useless paths. It is also a major challenge for all techniques in static analysis of programs, since the quality of the approximations they provide is lowered by data computed for paths that do not correspond to actual program runs.To overcome this problem, different methods have been proposed, like concolic testing or random testing based on the input domain. In path-biased random testing, paths are drawn according to a given distribution and their feasibility is checked in a second step. We present an algorithm that builds better approximations of the behavior of a program than its CFG, providing a transformed CFG, which still over-approximates the set of feasible paths but with fewer infeasible paths. This transformed graph is used for drawing paths at random.We modeled our graph transformations and formally proved, using the interactive theorem proving environment Isabelle/HOL, the key properties that establish the correctness of our approach.Our algorithm uses symbolic execution and constraint solving, which allows to detect whether some paths are infeasible. Since programs can contain loops, their graphs can contain cycles. In order to avoid to follow infinitely a cyclic path, we enrich symbolic execution with the detection of subsumptions. A subsumption can be interpreted as the fact that some node met during the analysis is a particular case of another node met previously: there is no need to explore the successors of the subsumed node: they are subsumed by the successors of the subsumer. Our algorithm has been implemented by a prototype, whose design closely follows said formalization, giving a good level of confidence in its correctness.In this thesis, we introduce the theoretical concepts on which our approach relies, its formalization in Isabelle/HOL, the algorithms our prototype implements and the various experiments done and results obtained using it.

Il existe plusieurs filtrations intéressantes définies sur la sous-algèbre de Cartan d'une algèbre de Lie simple complexe issues de contextes très variés : l'une est la filtration principale qui provient du dual de Langlands, une autre provient de l'algèbre de Clifford associée à une forme bilinéaire invariante non-dégénérée, une autre encore provient de l'algèbre symétrique et la projection de Chevalley, deux autres enfin proviennent de l'algèbre enveloppante et des projections de Harish-Chandra. Il est connu que toutes ces filtrations coïncident. Ceci résulte des travaux de Rohr, Joseph et Alekseev-Moreau. La relation remarquable entre les filtrations principale et de Clifford fut essentiellement conjecturée par Kostant. L'objectif de ce mémoire de thèse est de proposer une nouvelle démonstration de l'égalité entre les filtrations symétrique et enveloppante pour une algèbre de Lie simple de type A ou C. Conjointement au résultat et Rohr et le théorème d'Alekseev-Moreau, ceci fournit une nouvelle démonstration de la conjecture de Kostant, c'est-à-dire une nouvelle démonstration du théorème de Joseph. Notre démonstration est très différentes de la sienne. Le point clé est d'utiliser une description explicite des invariants via la représentation standard, ce qui est possible en types A et C. Nous décrivons alors les images de leurs différentielles en termes d'objects combinatoires, appelés des chemins pondérés, dans le graphe cristallin de la représentation standard. Les démonstrations pour les types A et C sont assez similaires, mais ne nouveaux phénomènes apparaissent en type C, ce qui rend la démonstration nettement plus délicate dans ce cas. / There are several interesting filtrations on the Cartan subalgebra of a complex simple Lie algebra coming from very different contexts: one is the principal filtration coming from the Langlands dual, one is coming from the Clifford algebra associated with a non-degenerate invariant bilinear form, one is coming from the symmetric algebra and the Chevalley projection, and two other ones are coming from the enveloping algebra and Harish-Chandra projections. It is known that all these filtrations coincide. This results from a combination of works of several authors (Rohr, Joseph, Alekseev-Moreau). The remarkable connection between the principal filtration and the Clifford filtration was essentially conjectured by Kostant. The purpose of this thesis is to establish a new correspondence between the enveloping filtration and the symmetric filtration for a simple Lie algebra of type A or C. Together with Rohr's result and Alekseev-Moreau theorem, this provides another proof of Kostant's conjecture for these types, that is, a new proof of Joseph's theorem. Our proof is very different from his approach. The starting point is to use an explicit description of invariants via the standard representation which is possible in types A and C. Then we describe the images of their differentials by the generalised Chevalley and Harish-Chandra projections in term of combinatorial objects, called weighted paths, in the crystal graph of the standard representation. The proofs for types A and C are quite similar, but there are new phenomenons in type C which makes the proof much more tricky in this case.

Cette thèse porte sur la question de l’intégration de l’espace ferroviaire européen, à partir d’une approche centrée sur les relations professionnelles communautaires qui se sont développées depuis le milieu des années 1980 entre représentants des salariés, des employeurs et des institutions publiques dans ce secteur. En s’appuyant surl’analyse de documents et de bases de données publiques, sur une enquête de terrain par entretien et par observation et sur le dépouillement d’archives, elle adopte une perspective sociohistorique sur ces évolutions, qui prend pour pivot l’analyse des activités du comité de dialogue social européen « chemins de fer ». Dans une première partie, nous soulignons que les évolutions du dialogue social « chemins de fer » ne peuvent pasêtre comprises indépendamment de la dynamique du dialogue social européen interprofessionnel, qui a notamment participé à la transformation du cadre institutionnel du dialogue social sectoriel et influé sur la nature des produits et sur les thématiques abordées par les acteurs du rail. Dans une seconde partie, nous montrons cependant que les activités les plus significatives dans ce secteur s’articulent à l’enjeu de l’intégration ferroviaire européenne, qui constitue l’un des objectifs clés de la politique européenne des transports. Elles aboutissent à la fois à une mise en débat des orientations générales de cette politique et à des activités participant à la construction d’un espace ferroviaire européen plus intégré : les acteurs ont ainsi participé à l’élaboration d’une législation communautaire dans le domaine de la certification professionnelle des cheminots mobiles (« permis de conduire » européen) et ont mené plusieurs initiatives marquant l’émergence d’une négociation collective européenne. Le développement de l’interopérabilité technique et économique du système ferroviaire a donc débouché sur la construction d’une interopérabilité sociale. Les acteurs européens sont ainsi parvenus à construire le niveau communautaire du système de relations professionnelles européen qui émerge actuellement dans le rail. / This PhD thesis deals with the integration of the European railway area in a perspective of industrial relations’ analysis. Based on a field survey by interview and observation and on analysis of public documents and archives, it adopts a socio-historical perspective, centered on the activities of railway sector’s European social dialogue committee. In a first part, we underline that “railways” EU social dialogue’s evolutions have to be understood in the light of interprofessional European social dialogue’s dynamic, as it has influenced the shaping of sectoral dialogue’s institutional framework as well as the nature of products and themes addressed in the railway sector. In a second part, we show however that the most significant activities in this sector are related to integration of European railways, one of EU railway policy’s key objectives. Industrial relations’ actors have both discussed the general orientations of this policy and taken part to the process of building an integrated railway area in Europe: they have participated to shape EU legislation on mobile railway workers’ professional certification(European “driving licence”) and have managed to conduct successfully in their sector Europeancollective bargaining processes. The development of technical and economical interoperability of EUrailway system has therefore led to the building of social interoperability. EU level actors have thusmanaged to build the community level of a European industrial relation system, currently emerging in the railway sector.