No description available.

La particule de reconnaissance du signal (signal recognition particle-SRP) et son récepteur (FtsY chez Escherichia coli) médiatise le processus simultané de traduction-ciblage de la protéine en dirigeant le complexe ribosome-nascent chain (RNCs) vers la membrane de destination. La reconnaissance par la SRP d'une charge RNC à transporter dépend de la présence de la partie N-terminale. L'assemblage de Ftsy au complexe RNC-PRS entraine plusieurs changements de configuration de SRP et de FtsY durant le cycle de direction. D'abord un stade « précoce » sans GTP est adopté. Celui-ci est stabilisé par le RNC. Ensuite une configuration « fermée » avec GTP est formée. Cette dernière peut s'activer pour hydrolyser GTP, elle entre alors dans sa configuration « active ». La succession de ces trois étapes conduit à la libération du complexe SRP-récepteur d'avec le ribosome et de sa protéine en cours de traduction, et leur mise à disposition au pore de la membrane. Dans ce projet, notre intérêt se limite à la traduction par le ribosome de la séquence signale EspP (RNCEspP). In vivo, EspP est une protéine dont le ciblage vers le récepteur membranaire se réalise après la traduction. Cependant il arrive que RNCEspP se lie au complexe SRP-FtsY, faisant échouer le ciblage. Nous avons étudié les bases structurales du rejet de RNCEspP par SRP et FtsY. Pour cela nous avons effectué la comparaison de la structure RNCEspP-SRP-FtsY obtenue par observation au cryo-microscope électronique avec d'autres complexes ribosome-SRP-récepteurs traduisant la charge FtsQ, qui est elle normalement ciblé par SRP. Nous avons cherché à observer la différence de structure entre les complexes SRP-FtsY dans les deux cas. Deux différences majeurs entre les complexes de ciblages contenants les séquences RNCFtsQ et RNCEspP ont été observés. Premièrement, dans le cas de la structure de RNCEspP le domaine M -Ffh est attaché à l'hélice 59 du ribosome, alors que celui-ci est détaché dans le cas de la structure de RNCFtsQ. Nous pensons que le domaine M empêche la libération de la séquence de signal, étape nécessaire à la réalisation du ciblage. Deuxièmement, dans le cas de la structure du complexe avec RNCEspP l'arrangement Ffh-FtsY avec le domaine NG était flexible. Ceci indiquerait que le complexe “précoce” formé sur RNCEspP est moins stable que celui formé sur RNCFtsQ. Une étude biochimique utilisant le transfert d'énergie via résonance fluorescente a corroboré ce résultat, montrant que FTS Y est lié avec une affinité moindre dans le cas du complexe précoce formé sur RNCEspP et que la reconfiguration au stade de complexe fermé est moins efficace. Une analyse biochimique plus poussée des variantes de la séquence de EspP montre que la partie N-Terminale de la séquence est la principale cause de rejet du cycle de ciblage via SRP.Dans un second projet, nous avons étudié la configuration “fermée” de SRP et ftsY en complexe avec une charge RNC stabilisée par un analogue non-hydrolysable de GTP (GMP-PCP). Pour franchir la barrière cinétique qui permet de passer du complexe précoce au complexe fermé, nous avons utilisé une version tronquée de FtsY, à laquelle la séquence terminale avait été amputée de tout le domaine acide (A-) ainsi que de la première hélice alpha du domaine NG. De plus, pour la formation du complexe, nous avons utilisé une construction contenant les 50 premiers acides aminés du leader peptidase (RNCLep50). En l'absence de nucléotides, notre reconstruction au cryo-EM a montré une configuration similaire à celle du stade précoce, dans laquelle Ftsy et Ffh- domaine NG, sont proche du tetraloop de la 4.5 S ARN. Une incubation avec GMP-PCP induit un détachement du domaine NG d'avec la queue du tetraloop. Il semblerait que les domaines NG soient flexibles dans l'état clos, et non attaché à la terminaison ouverte de l'ARN. / The signal recognition particle (SRP) and its receptor (FtsY in Escherichia coli) mediate co-translational protein targeting by delivering ribosome nascent chain complexes (RNCs) to the target membrane. Recognition of an RNC cargo by SRP is dependent on an N-terminal signal sequence. Binding of FtsY to the RNC-SRP complex leads to several conformational changes of SRP and FtsY during the targeting cycle: first, an “early” GTP-independent state is adopted which is stabilized by the RNC, subsequently a “closed” GTP- dependent conformation is formed which can activate itself to hydrolyze GTP (the “activated” state). Faithful completion of all three steps leads to release of the cargo from SRP-FtsY and hand over of the RNC to the translocation pore.It has been shown for E. coli that cargos can be rejected from the SRP pathway during all targeting steps. In the first project, our interest concentrates on ribosomes translating the EspP signal sequence (RNCEspP). In vivo, EspP is a post-translationally targeted protein, but RNCEspP has been shown to be bound by SRP and FtsY leading to a non-productive “early”-like RNCEspP-SRP-FtsY complex. Using single particle cryo-electron microscopy (EM), we analysed the structural basis for the rejection of RNCEspP by SRP and FtsY. Comparison of our RNCEspP-SRP-FtsY cryo-EM structure to other available cryo-EM structures of co-translational targeting complexes containing the correct cargo RNCFtsQ unravelled differences in the SRP-FtsY structure between a correct cargo and an incorrect cargo. Two major differences between the targeting complexes containing the cargos RNCFtsQ and RNCEspP were observed: first, the Ffh M-domain was attached to ribosomal RNA helix 59 of RNCEspP, while it was detached from this site in the case of RNCFtsQ. It could be that such an ordered M-domain is hampering the release of the signal sequence which is required for successful completion of targeting. Second, the Ffh-FtsY NG-domain arrangement was flexible in the complex with RNCEspP in comparison to RNCFtsQ indicating that the "early"-like complex formed on RNCEspP is less stable. Biochemical data using fluorescence resonance energy transfer corroborated these results, showing that FtsY is bound with lower affinity in the RNCEspP “early” complex and that the rearrangement to the “closed” conformation is less efficient. Further biochemical analysis of EspP signal sequence variants showed that mainly the N-terminal extension of the EspP signal sequence is responsible for its rejection from the SRP pathway.

Dans cette thèse, nous présentons des approches formelles permettant de simplifier la modélisation et la preuve du calcul distribué. Un système distribué est défini par une collection d’entités de calcul autonomes,qui communiquent ensemble pour accomplir une tâche commune. Chaque entité exécute localement son calcul et ne peut interagir qu’avec ses voisins.Le développement et la preuve du calcul distribué est un défi qui nécessite l’utilisation de méthodes et outils avancés. Dans nos travaux de thèse,nous étudions quelques problèmes fondamentaux du distribués, en utilisant Event-B, et nous proposons des schémas de preuve basés sur une approche“correct-par-construction”. Nous considérons un système distribué défini par réseau fiable, de processus anonymes et avec un modèle de communication basé sur l’échange de messages. Dans certains cas, nous faisons abstraction du modèle de communications en utilisant le modèle des calculs locaux. Nous nous focalisons d’abord sur le problème de détection de terminaison du calcul distribué. Nous proposons un patron formel permettant de transformer des algorithmes “avec détection de terminaison locale” en des algorithmes“avec détection de terminaison globale”. Ensuite, nous explicitons les preuves de correction d’un algorithme d’énumération. Nous proposons un développement formel qui servirait de point de départ aux calculs qui nécessitent l’hypothèse d’identification unique des processus. Enfin, nous étudions le problème du snapshot et du calcul d’état global. Nous proposons une solution basée sur une composition d’algorithmes existants. / In this work, we propose formal approaches for modeling andproving distributed algorithms. Such computations are designed to run oninterconnected autonomous computing entities for achieving a common task :each entity executes asynchronously the same code and interacts locally withits immediate neighbors. Correctness of distributed algorithms is a difficulttask and requires advancing methods and tools. In this thesis, we focus onsome basic problems of distributed computing, and we propose Event-B solutionsbased on the ”correct-by-construction” approach. We consider reliablesystems. We also assume that the network is anonymous and processes communicatewith asynchronous messages. In some cases, we refer to local computationsmodel to provide an abstraction of the distributed computations.We propose a formal framework enhancing the termination detection propertyof distributed algorithms. By relying on refinement and composition,we show that an algorithm specified with “local termination detection”, canbe reused in order to compute the same algorithm with “global terminationdetection”. We then focus on the enumeration problem : we start with anabstract initial specification of the problem, and we enrich it gradually bya progressive and incremental refinement. The computed result constitutesbasic initial steps of others distributed algorithms which assume that processeshave unique identifiers. We therefore focus on snapshot problems, andwe propose to investigate how existing algorithms can be composed, withrefinement, in order to compute a global state in an anonymous network.

Chez les eucaryotes, la maturation de l’extrémité 3’ des ARNs messagers a lieu lors de la transcription et regroupe deux étapes : le clivage endonucléolytique du transcrit au niveau d’un site spécifique et l’ajout d’une queue poly(A) sur le fragment en amont du site de clivage. Chez S. cerevisiae, le complexe de polyadénylation est formé par 20 protéines, regroupées principalement en deux sous-complexes : CF IA et CPF. Nous nous intéressons plus spécifiquement à Pcf11, sous-unité du complexe CF IA. Pcf11 est formé de sept sous-domaines, mais la fonction d’une grande partie de la protéine n’est pour l’instant pas connue. Par exemple, aucune fonction n’est associée à la région située entre le domaine d’interaction avec le CTD de l’ARN polymérase II (CID) et une répétion de 20 résidus glutamines. Récemment, la structure de ce domaine, appelé 2nd NTD a été décrite. Pour essayer de comprendre la fonction du 2nd NTD et des motifs liant le zinc encadrant le domaine d’interaction avec Clp1, nous avons mis en place une stratégie systématique de mutagénèse, soit par délétions, soit par mutations ponctuelles. Le 2nd NTD est formé de trois hélices α et interagit avec l’ARN. La délétion de ce domaine conduit à un phénotype de croissance lente chez la levure et un défaut de terminaison de transcription des snoRNAs. Malgré une similarité de structure et de fonction, le 2nd NTD présenterait une fonction indépendante. La fonction des motifs liant le zinc n’est pour l’instant pas connue. Cependant, la mutation de l’un de ces deux motifs conduit à un défaut de clivage et de polyadénylation in vitro. La mutation des deux motifs est létale chez la levure. / In eukaryotes, poly (A) tails are added to nuclear pre-mRNA 3'-ends in the two steps of cleavage and polyadenylation. This co-transcriptional processing requires the activity of a large protein complex comprising at least 20 different polypeptides in yeast organized primarily into the two factors CF IA and CPF. We are interested in the functional characterization of Pcf11, a CF IA subunit. The Pcf11 protein is organized into seven different domains, but here is still a large portion of the polypeptide that has not yet been characterized. For example the region from the end of the CTD interaction domain (CID) to an uninterrupted stretch of 20 glutamine residues has no known function. Recently, the structure of this region, called the 2nd NTD have been characterized. To gain insight into the function of the 2nd NTD and the two zinc fingers motif surrounding the Clp1 interaction domain, we have employed a systematic strategy of mutagenesis, either by deletion or via point mutations. The 2nd NTD is a folded domain composed of three α-helices. The deletion of this domain induced a severe defect of growth in yeast and impaired transcription termination of snoRNAs. Despite its similarity in structure and function with the CID, the 2nd NTD seems to act like an independent RNA binding domain. We don’t know yet the real function of the two zinc fingers motif at the C-terminal region of Pcf11, but the mutation of Cystein residues into serine of one of the two motifs impaired cleavage and polyadenylation. The mutation of the first motif is less harmful than the mutation of the second motif. The simultaneous mutation is lethal in yeast.

L’objectif général de cette thèse est le développement de méthodes mathématiques correctes et efficaces en pratique pour prouver automatiquement la correction de logiciels. Plus précisément, cette thèse est fondée sur la théorie de l’interprétation abstraite, un cadre mathématique puissant pour l’approximation du comportement des programmes. En particulier, cette thèse se concentre sur la preuve des propriétés de vivacité des programmes, qui représentent des conditions qui doivent être réalisés ultimement ou de manière répétée pendant l’exécution du programme. La terminaison des programmes est la propriété de vivacité la plus fréquemment considérée. Cette thèse conçoit des nouvelles approximations, afin de déduire automatiquement des conditions suffisantes pour la terminaison des programmes et synthétiser des fonctions de rang définies par morceaux, qui fournissent des bornes supérieures sur le temps d’attente avant la terminaison. Les approximations sont paramétriques dans le choix entre l’expressivité et le coût des approximations sous-jacentes, qui maintiennent des informations sur l’ensemble des valeurs possibles des variables du programme ainsi que les relations numériques possibles entre elles. Cette thèse développe également un cadre d’interprétation abstraite pour prouver des propriétés de vivacité, qui vient comme une généralisation du cadre proposé pour la terminaison. En particulier, le cadre est dédié à des propriétés de vivacité exprimées dans la logique temporelle, qui sont utilisées pour s’assurer qu’un événement souhaitable se produit une fois ou une infinité de fois au cours de l’exécution du programme. Comme pour la terminaison,des fonctions de rang définies par morceaux sont utilisées pour déduire des préconditions suffisantes pour ces propriétés, et fournir des bornes supérieures sur le temps d’attente avant un événement souhaitable. Les résultats présentés dans cette thèse ont été mis en œuvre dans un prototype d’analyseur. Les résultats expérimentaux montrent qu’il donne de bons résultats sur une grande variété de programmes, il est compétitif avec l’état de l’art, et il est capable d’analyser des programmes qui sont hors de la portée des méthodes existantes. / The overall aim of this thesis is the development of mathematically sound and practically efficient methods for automatically proving the correctness of computer software. More specifically, this thesis is grounded in the theory of abstract interpretation, a powerful mathematical framework for approximating the behavior of programs. In particular, this thesis focuses on provingprogram liveness properties, which represent requirements that must be eventually or repeatedly realized during program execution. Program termination is the most prominent liveness property. This thesis designs new program approximations, in order to automatically infer sufficient preconditions for program termination and synthesize so called piecewisedefined ranking functions, which provide upper bounds on the waiting time before termination. The approximations are parametric in the choice between the expressivity and the cost of the underlying approximations, which maintain information about the set of possible values of the program variables along with the possible numerical relationships between them. This thesis also contributes an abstract interpretation framework for proving liveness properties, which comes as a generalization of the framework proposedfor termination. In particular, the framework is dedicated to liveness properties expressed in temporal logic, which are used to ensure that some desirable event happens once or infinitely many times during program execution. As for program termination, piecewise-defined ranking functions are used to infer sufficient preconditions for these properties, and to provide upper boundson the waiting time before a desirable event. The results presented in this thesis have been implemented into a prototype analyzer. Experimental results show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art, and is able to analyze programs that are out of the reach of existing methods.

Peaks andThe main subject of this thesis is diagram rewriting.This is a generalisation to dimension~$2$ of word rewriting (in dimension~$1$). In a first time, we give the first convergent diagrammatic presentation of the PRO of linear maps in arbitrary field. Then we study the convergent diagrammatic presentation of matrix of isometries of $RR^n$. We focus especially on a rule similar to the Yang-Baxter equation, described by a certain map $h$. We use the confluence of critical the parametric diagrams, To study the algebraic properties of $h$, Finally, we present the $Sigma$-diagrams, an alternative approach for calculation in bialgebras. We illustrate this approach with examples. The last two chapters have been already published: Diagram rewriting for orthogonal matrices: a study of critical peaks, avec Yves Lafont, Lecture Notes in Computer Science 5117, p. 232-245, 2008 Properties of co-operations: diagrammatic proofs, Mathematical Structures in Computer Science 22(6), p. 970-986, 2012. / The main subject of this thesis is diagram rewriting.This is a generalisation to dimension~$2$ of word rewriting (in dimension~$1$). In a first time, we give the first convergent diagrammatic presentation of the PRO of linear maps in arbitrary field. Then we study the convergent diagrammatic presentation of matrix of isometries of $RR^n$. We focus especially on a rule similar to the Yang-Baxter equation, described by a certain map $h$. We use the confluence of criticalthe parametric diagrams, To study the algebraic properties of $h$, Finally, we present the $Sigma$-diagrams, an alternative approach for calculation in bialgebras. We illustrate this approach with examples. The last two chapters have been already published: Diagram rewriting for orthogonal matrices: a study of critical peaks, avec Yves Lafont, Lecture Notes in Computer Science 5117, p. 232-245, 2008 Properties of co-operations: diagrammatic proofs, Mathematical Structures in Computer Science 22(6), p. 970-986, 2012.

Nous proposons une technique de dépliage pour vérifier les systèmes concurrents infinis bien structurés. Certaines propriétés d'intérêt comme la bornitude, la couverture et la terminaison sont décidables grâce à la bonne structure de ces systèmes. D'autre part, le dépliage réduit efficacement l'explosion combinatoire en exploitant l'ordre partiel entre les événements des systèmes concurrents. Nous proposons une modélisation par structure d'événements pour des systèmes bien structurés élémentaires, tels les compteurs et les files de communication. Le dépliage d'un réseau de structures d'événements étant une structure d'événements, nous proposons ensuite une approche hiérarchique à la modélisation et à la vérification des systèmes, qui préserve la bonne structure. Enfin, nous proposons une technique d'élimination des événements redondants. La mise en œuvre de notre approche dans l'outil ESU nous permet de conclure à son efficacité. / We propose an unfolding technique for verifying concurrent infinite-state systems that are well-structured. Some properties of interest such as boundedness, coverability and termination are decidable thanks to the well-structure of these systems. Moreover, the unfolding effectively reduces the combinatorial explosion by exploiting the partial order between events of concurrent systems. We propose a modelization using event structures for basic well-structured systems, such as counters and communication channels. As the unfolding of a synchronized product of event structures is an event structure, we obtain a hierarchical approach to modeling as well as to verifying systems, which preserves the well-structure. Finally, we propose a technique for eliminating redundant events. The implementation of our approach in the ESU tool allows us to conclude on its efficiency.

Le but de cette thèse est de caractériser les variations climatiques des derniers 200 ka à travers l'étude de quatre spéléothèmes du sud de la France, datés par U-Th. Nous nous sommes focalisés sur l'étude des stades isotopiques marins MIS 6, 5 et 3. Les principaux résultats obtenus sont les suivants : - mise en évidence d'oscillations milléniales au MIS6 entre 175 et 165 ka. L'enregistrement isotopique haute résolution (10 à 300 ans) de la base du plancher stalagmitique de la grotte de Villars indique pour la première fois dans la région ces oscillations climatiques rapides qui peuvent être mises en relation avec des figures similaires récemment mises à jour par les concrétions chinoises. - estimation de l'amplitude du réchauffement associée à l'avant-dernière déglaciation. La confrontation du δ18Oc de la calcite, du δ18O des inclusions fluides et du ∆47 de la calcite suggère que (1) si l'équilibre isotopique a été satisfait, le réchauffement associé à la Terminaison II serait de 20°C, (2) si on considère un effet cinétique alors le réchauffement corrigé de cet effet serait de 14°C. La constance de la composition de l'eau de l'infiltration pendant cette déglaciation s'explique par le jeu des différents facteurs influant sur ce paramètre. - amélioration de la chronologie et de la caractérisation dans le SW de la France des événements climatiques milléniaux de la dernière glaciation (MIS3). L'enregistrement de la stalagmite Vil14 daté par MC-ICP-MS constitue désormais la meilleure chronologie de cette période dans la grotte de Villars et permet d'attribuer un âge précis aux limites des interstades (13, 12 et fin du 14). La fin des interstades identifiés était manifestement associée à un refroidissement abrupt et à l'installation d'un permafrost de courte durée. La cessation de croissance définitive de cet échantillon simultanément aux deux autres confirme le durcissement du refroidissement du MIS3 vers 30ka. En multipliant ce type de données quantifiées et datées de façon absolue, on contribue à la meilleure compréhension des mécanismes climatiques.

La sénescence est considérée comme un mécanisme de suppression tumorale puisque les cellules potentiellement dangereuses, activent leurs protéines de sauvegarde pour arrêter leur prolifération. Les protéines de sauvegarde telles que RB et p53 sont activées suite à différents stress comme des dommages à l’ADN, le raccourcissement des télomères ou l’induction oncogénique. Les cellules sénescentes restent métaboliquement actives, subissent des modifications dans leur expression génique, et sécrètent des cytokines et des chimiokines qui ont des effets paracrines pro-oncogéniques, mais peuvent également contribuer à la stabilité de l’arrêt du cycle cellulaire dans la sénescence de façon autocrine. Une des particularités du phénotype sénescent est la dégradation sélective des protéines dépendante de l’ubiquitination et du protéasome. Parmi les cibles de dégradation se trouvent des protéines impliquées dans la biogenèse du ribosome, ainsi que celles d’autres voies cellulaires requises pour la croissance de cellules cancéreuses. Ceci est lié à un stress nucléolaire qui affecte la biogenèse du ribosome, menant à l’accumulation, dans le nucléoplasme ou le nucléole, de protéines ribosomiques. Ce comportement suggère que les ribosomes des cellules sénescentes seraient structurellement différents. Par conséquent, ceci pourrait entrainer des effets sur leurs capacités à réguler l’initiation, l’élongation et/ou la terminaison de la traduction des ARN messagers (ARNm). Par ailleurs, la déplétion de certaines protéines impliquées dans la ribogenèse, ainsi que la surexpression de protéines ribosomiques telles que RPS14/uS11 amènent à la sénescence. Malgré le stress nucléolaire et les défauts de ribogenèse associés à la sénescence, les cellules sénescentes présentent des niveaux de translecture du codon d’arrêt très diminué, suggérant l’existence de défauts de production de protéines allongées en C-terminal. Nous émettons l’hypothèse que les défauts de la ribogenèse affecteraient la fonction des protéines ribosomiques et des ribosomes. Cette perturbation aurait un impact sur le rôle de suppresseur tumoral de la sénescence. Le premier objectif de cette thèse consiste à démontrer le rôle de RPL22/eL22 en tant que régulateur du cycle cellulaire et inducteur de la sénescence. Le deuxième but est de démontrer que, malgré la perturbation nucléolaire, les ribosomes des fibroblastes sénescents reconnaissent les codons d’arrêt de façon plus efficace que les ribosomes des cellules transformées, ou des cellules normales en prolifération. Nous avons démontré que le phénotype de sénescence peut être induit quand l’expression de RPL22/eL22 est augmentée. RPL22/eL22 s’accumule principalement dans le nucléole, de manière différente de RPS14/uS11, dont l’accumulation est nucléoplasmique. En effectuant des essais kinases in vitro, nous avons montré que RPL22/eL22, tout comme RPS14/uS11, peuvent interagir et inhiber le complexe CDK4-Cycline D1 afin d’activer la voie de RB et établir l’arrêt du cycle cellulaire et la sénescence. Afin de démontrer la fidélité de la terminaison de la traduction dans les cellules sénescentes, nous avons utilisé un système de rapporteurs de luciférases, pour détecter les erreurs de translecture ainsi que pour avoir un contrôle interne du système. L’inactivation de la voie du suppresseur tumoral RB par surexpression de CDK4 ou de l’oncoprotéine virale E7, nous a permis d’observer l’augmentation de la translecture dans les cellules sénescentes. Tandis que l’activation de la voie de suppression tumorale RB, à l’aide du suppresseur de tumeur PML, de la surexpression de RPL22/eL22 et de RPS14/uS11, ainsi que de l’utilisation de Palbociclib (PD-0332991), un inhibiteur des kinases CDK4/6, a montré une réduction des erreurs de translecture. Ces résultats indiquent une nouvelle fonction des protéines du ribosome en tant que suppresseurs de tumeur, permettant d’inhiber les erreurs de translecture du codon d’arrêt de façon dépendante de la voie de RB. Ces travaux suggèrent que de petites molécules ou peptides pourraient simuler les fonctions inhibitrices de ces protéines ribosomiques afin de traiter certains cancers où la voie de RB est activable. / Senescence is considered a mechanism for tumor suppression since potentially dangerous cells activate their protective proteins to stop their proliferation. Safeguard proteins such as RB and p53 are activated as a result of stress such as DNA damage, telomere shortening or oncogenic induction. Senescent cells are metabolically active, they undergo changes in their gene expression and secrete cytokines and chemokines with pro-oncogenic paracrine effects, but which can also contribute to the stability of the senescent cell cycle arrest in an autocrine way. One of the peculiarities of the senescent phenotype is the selective ubiquitination and proteasome dependent-degradation of proteins involved in ribosome biogenesis and other cellular pathways required for cancer cell growth, leading to the accumulation, in the nucleoplasm or nucleolus, of ribosomal proteins. This behavior suggests that the ribosomes of senescent cells are structurally different. Therefore, this could have effects on their ability to regulate the initiation, elongation and/or translation termination of messenger RNAs (mRNAs). Moreover, the depletion of some proteins involved in ribogenesis, as well as the overexpression of ribosomal proteins such as RPS14/uS11 lead to senescence. Despite nucleolar stress and ribogenesis defects associated to senescence, global translation does not seem to be affected in senescence. Strikingly, senescent cells have reduced translational readthrough suggesting that they have defects in the production of C-terminal extended proteins. We hypothesize that defects in ribogenesis would affect the function of ribosomal proteins and ribosomes influencing the tumor suppressor role of senescence. The first aim of this thesis is to demonstrate the role of RPL22/eL22 as a regulator of the cell cycle and senescence inducer. The second aim of this thesis is to demonstrate that, despite the nucleolar disruption, the ribosomes of senescent fibroblasts recognize stop codons more efficiently than ribosomes from transformed cells, but also than ribosomes from proliferating normal cells. We found that the senescent phenotype can be induced by enhancing the expression of RPL22/eL22. RPL22/eL22 accumulates mainly in the nucleolus, unlike RPS14/uS11, whose accumulation is nucleoplasmic. By performing an in vitro kinase assay, we showed that RPL22/eL22, just like RPS14/uS11, can interact and inhibit the CDK4-Cyclin D1 complex in order to activate the RB pathway and establish cellular arrest and senescence. To assess translation termination accuracy in senescent cells, we used a system of luciferase reporters to measure the fidelity of translation termination. Inactivation of the RB tumor suppressor pathway using CDK4 or the viral oncoprotein E7 also increased readthrough in senescent cells while overexpression of PML, a tumor suppressor that activates the RB pathway, overexpression of RPL22/eL22 and RPS14/uS11, as well as the use of Palbociclib (PD-0332991), a CDK4/6 inhibitor, reduce readthrough errors. These results indicate a novel function of ribosomal proteins as tumor suppressors, making it possible to inhibit translational readthrough errors, in a RB-dependent pathway. This work suggests that small molecules or peptides could mimic the inhibitory functions of these ribosomal proteins in order to treat cancers where the RB pathway is activatable.

Les travaux présentés dans cette thèse sont lies aux problèmes de vérification de l'atteignabilité et de la terminaison de programmes qui manipulent des données entières non-bornées. On décrit une nouvelle méthode de vérification basée sur une technique d'accélération de boucle, qui calcule, de manière exacte, la clôture transitive d'une relation arithmétique. D'abord, on introduit un algorithme d'accélération de boucle qui peut calculer, en quelques secondes, des clôtures transitives pour des relations de l'ordre d'une centaine de variables. Ensuite, on présente une méthode d'analyse de l'atteignabilité, qui manipule des relations entre les variables entières d'un programme, et applique l'accélération pour le calcul des relations entrée-sortie des procédures, de façon modulaire. Une approche alternative pour l'analyse de l'atteignabilité, présentée également dans cette thèse, intègre l'accélération avec l'abstraction par prédicats, afin de traiter le problème de divergence de cette dernière. Ces deux méthodes ont été évaluées de manière pratique, sur un nombre important d'exemples, qui étaient, jusqu'a présent, hors de la portée des outils d'analyse existants. Dernièrement, on a étudié le problème de la terminaison pour certaines classes de boucles de programme, et on a montré la décidabilité pour les relations étudiées. Pour ces classes de relations arithmétiques, on présente un algorithme qui s'exécute en temps au plus polynomial, et qui calcule l'ensemble d'états qui peuvent générer une exécution infinie. Ensuite on a intégré cet algorithme dans une méthode d'analyse de la terminaison pour des programmes qui manipulent des données entières. / This work presents novel methods for verification of reachability and termination properties of programs that manipulate unbounded integer data. Most of these methods are based on acceleration techniques which compute transitive closures of program loops. We first present an algorithm that accelerates several classes of integer relations and show that the new method performs up to four orders of magnitude better than the previous ones. On the theoretical side, our framework provides a common solution to the acceleration problem by proving that the considered classes of relations are periodic. Subsequently, we introduce a semi-algorithmic reachability analysis technique that tracks relations between variables of integer programs and applies the proposed acceleration algorithm to compute summaries of procedures in a modular way. Next, we present an alternative approach to reachability analysis that integrates predicate abstraction with our acceleration techniques to increase the likelihood of convergence of the algorithm. We evaluate these algorithms and show that they can handle a number of complex integer programs where previous approaches failed. Finally, we study the termination problem for several classes of program loops and show that it is decidable. Moreover, for some of these classes, we design a polynomial time algorithm that computes the exact set of program configurations from which non-terminating runs exist. We further integrate this algorithm into a semi-algorithmic method that analyzes termination of integer programs, and show that the resulting technique can verify termination properties of several non-trivial integer programs. / Tato pr´ace pˇredstavuje nov´e metody pro verifikaci program°u pracuj´ıc´ıch s neomezen´ymiceloˇc´ıslen´ymi promˇenn´ymi, konkr´etnˇe metody pro anal´yzu dosaˇzitelnosti a koneˇcnosti.Vˇetˇsina tˇechto metod je zaloˇzena na akceleraˇcn´ıch technik´ach, kter´e poˇc´ıtaj´ı tranzitivn´ıuz´avˇery cykl°u programu.V pr´aci je nejprve pˇredstaven algoritmus pro akceleraci nˇekolika tˇr´ıd celoˇc´ıseln´ychrelac´ı. Tento algoritmus je aˇz o ˇctyˇri ˇr´ady rychlejˇs´ı neˇz existuj´ıc´ı techniky. Z teoretick´ehohlediska pr´ace dokazuje, ˇze uvaˇzovan´e tˇr´ıdy relac´ı jsou periodick´e a poskytuje tud´ıˇzjednotn´e ˇreˇsen´ı prol´emu akcelerace.Pr´ace d´ale pˇredstavuje semi-algoritmus pro anal´yzu dosaˇzitelnosti celoˇc´ıseln´ych program°u, kter´y sleduje relace mezi promˇenn´ymi programu a aplikuje akceleraˇcn´ı technikyza ´uˇcelem modul´arn´ıho v´ypoˇctu souhrn°u procedur. D´ale je v pr´aci navrˇzen alternativn´ıalgoritmus pro anal´yzu dosaˇzitelnosti, kter´y integruje predik´atovou abstrakci s accelerac´ıs c´ılem zv´yˇsit pravdˇepodobnost konvergence v´ypoˇctu. Proveden´e experimenty ukazuj´ı, ˇzeoba algoritmy lze ´uspˇeˇsnˇe aplikovat k verifikaci program°u, na kter´ych pˇredchoz´ı metodyselh´avaly.Pr´ace se rovnˇeˇz zab´yv´a probl´emem koneˇcnosti bˇehu program°u a dokazuje, ˇze tentoprobl´em je rozhodnuteln´y pro nˇekolik tˇr´ıd celoˇc´ıseln´ych relac´ı. Pro nˇekter´e z tˇechto tˇr´ıdrelac´ı je v pr´aci navrˇzen algoritmus, kter´y v polynomi´aln´ım ˇcase vypoˇc´ıt´a mnoˇzinu vˇsechkonfigurac´ı programu, z nichˇz existuje nekoneˇcn´y bˇeh. Tento algoritmus je integrov´ando metody, kter´a analyzuje koneˇcnost bˇeh°u celoˇc´ıseln´ych program°u. Efektivnost t´etometody je demonstrov´ana na nˇekolika netrivi´aln´ıch celoˇc´ıseln´ych programech.