Cette thèse s'intéresse à la démonstration automatique de la validité de formules mathématiques issues de la preuve de programmes. Elle se focalise tout particulièrement sur la Satisfiabilité Modulo Théories (SMT): un jeune domaine de recherche qui a connu de grands progrès durant la dernière décennie. Les démonstrateurs de cette famille ont des applications diverses dans la conception de microprocesseurs, la preuve de programmes, le model-checking, etc.Les démonstrateurs SMT offrent un bon compromis entre l'expressivité et l'efficacité. Ils reposent sur une coopération étroite d'un solveur SAT avec une combinaison de procédures de décision pour des théories spécifiques comme la théorie de l'égalité libre avec des symboles non interprétés, l'arithmétique linéaire sur les entiers et les rationnels, et la théorie des tableaux.L'objectif de cette thèse est d'améliorer l'efficacité et l'expressivité du démonstrateur SMT Alt-Ergo. Pour cela, nous proposons une nouvelle procédure de décision pour la théorie de l'arithmétique linéaire sur les entiers. Cette procédure est inspirée par la méthode de Fourier-Motzkin, mais elle utilise un simplexe sur les rationnels pour effectuer les calculs en pratique. Nous proposons également un nouveau mécanisme de combinaison, capable de raisonner dans l'union de la théorie de l'égalité libre, la théorie AC des symboles associatifs et commutatifs et une théorie arbitraire deShostak. Ce mécanisme est une extension modulaire et non intrusive de la procédure de completion close modulo AC avec la théorie de Shostak. Aussi, nous avons étendu Alt-Ergo avec des procédures de décision existantes pour y intégrer d'autres théories intéressantes comme la théorie de types de données énumérés et la théorie des tableaux. Enfin, nous avons exploré des techniques de simplification de formules en amont et l'amélioration de son solveur SAT. / This thesis tackles the problem of automatically proving the validity of mathematical formulas generated by program verification tools. In particular, it focuses on Satisfiability Modulo Theories (SMT): a young research topic that has seen great advances during the last decade. The solvers of this family have various applications in hardware design, program verification, model checking, etc.SMT solvers offer a good compromise between expressiveness and efficiency. They rely on a tight cooperation between a SAT solver and a combination of decision procedures for specific theories, such as the free theory of equality with uninterpreted symbols, linear arithmetic over integers and rationals, or the theory of arrays.This thesis aims at improving the efficiency and the expressiveness of the Alt-Ergo SMT solver. For that, we designed a new decision procedure for the theory of linear integer arithmetic. This procedure is inspired by Fourier-Motzkin's method, but it uses a rational simplex to perform computations in practice. We have also designed a new combination framework, capable of reasoning in the union of the free theory of equality, the AC theory of associative and commutativesymbols, and an arbitrary signature-disjoint Shostak theory. This framework is a modular and non-intrusive extension of the ground AC completion procedure with the given Shostak theory. In addition, we have extended Alt-Ergo with existing decision procedures to integrate additional interesting theories, such as the theory of enumerated data types and the theory of arrays. Finally, we have explored preprocessing techniques for formulas simplification as well as the enhancement of Alt-Ergo's SAT solver.

Dans le cadre industriel et académique, les méthodologies de développement logiciel exploitent de plus en plus le concept de “modèle” afin d’appréhender la complexité des systèmes temps réel critiques. En particulier, celles-ci définissent une étape dans laquelle un modèle fonctionnel, conçu comme un graphe de blocs fonctionnels communiquant via des échanges de signaux de données, est déployé sur un modèle de plateforme d’exécution matérielle et un modèle de plateforme d’exécution logicielle composé de tâches et de messages. Cette étape appelée étape de déploiement, permet d’établir une architecture opérationnelle du système nécessitant une validation des propriétés temporelles du système. Dans le contexte des systèmes temps réel dirigés par les évènements, la vérification des propriétés temporelles est réalisée à l’aide de l’analyse d’ordonnançabilité basée sur l’analyse des temps de réponse. Chaque choix de déploiement effectué a un impact essentiel sur la validité et la qualité du système. Néanmoins, les méthodologies existantes n’offrent pas de support permettant de guider le concepteur d’applications durant l’exploration de l’espace des architectures possibles. L’objectif de ces travaux de thèse consiste à mettre en place des techniques d’analyse et de synthèse automatiques permettant de guider le concepteur vers une architecture opérationnelle valide et optimisée par rapport aux performances du système. Notre proposition est dédiée à l’exploration de l’espace des architectures en tenant compte à la fois des quatre degrés de liberté déterminés durant la phase de déploiement, à savoir (j) le placement des éléments fonctionnels sur les éléments de calcul et de communication de la plateforme d’exécution, (ii) le partitionnement des éléments fonctionnels en tâches temps réel et des signaux de données en messages, (iii) l’affectation de priorités d’exécution aux tâches et aux messages du système et (iv) l’attribution du mécanisme de protection des données partagées pour les systèmes temps réel périodiques. Nous nous intéressons principalement à la satisfaction des contraintes temporelles et celles liées aux capacités des ressources de la plateforme cible. De plus, nous considérons l’optimisation des latences de bout-en-bout et la consommation mémoire. Les approches d’exploration architecturale présentées dans cette thèse sont basées sur la technique d’optimisation PLNE (programmation linéaire en nombres entiers) et concernent à la fois les applications activées périodiquement et celles dont l’activation est pilotée par les données. Contrairement à de nombreuses approches antérieures fournissant une solution partielle au problème de déploiement, les méthodes proposées considèrent l’ensemble du problème de déploiement. Les approches proposées dans cette thèse sont évaluées à l’aide d’applications génériques et industrielles. / Modern development methodologies from the industry and the academia exploit more and more the ”model” concept to address the complexity of critical real-time systems. These methodologies define a key stage in which the functional model, designed as a network of function blocks communicating through exchanged data signals, is deployed onto a hardware execution platform model and implemented in a software model consisting of a set of tasks and messages. This stage so-called deployment stage allows establishment of an operational architecture of the system, thus it requires evaluation and validation of the temporal properties of the system. In the context of event-driven real-time systems, the verification of temporal properties is performed using the schedulability analysis based on the response time analysis. Each deployment choice has an essential impact on the validity and the quality of the system. However, the existing methodologies do not provide supportto guide the designer of applications in the exploration of the operational architectures space. The objective of this thesis is to develop techniques for analysis and automatic synthesis of a valid operational architecture optimized with respect to the system performances. Our proposition is dedicated to the exploration of architectures space considering at the same time the four degrees of freedom determined during the deployment phase, (i) the placement of functional elements on the computing and communication resources of the execution platform, (ii) the partitioning of function elements into real time tasks and data signals into messages, (iii) the priority assignment to system tasks and messages and (iv) the assignment of shared data protection mechanism for periodic real-time systems. We are mainly interested in meeting temporal constraints and memory capacity of the target platform. In addition, we are focusing on the optimization of end-to-end latency and memory consumption. The design space exploration approaches presented in this thesis are based on the MILP (Mixed Integer Linear programming) optimization technique and concern at the same time time-driven and data-driven applications. Unlike many earlier approaches providing a partial solution to the deployment problem, our methods consider the whole deployment problem. The proposed approaches in this thesis are evaluated using both synthetic and industrial applications.

Le souhait d’augmenter la part des énergies renouvelables dans le mix énergétique entraine une augmentation des parts des énergies volatiles et non pilotables, et rend donc l’équilibre offre-demande difficile à satisfaire. Une façon d’intégrer ces énergies dans le réseau électrique actuel est d’utiliser de petits moyens de production, de consommation et de stockage répartis sur tout le territoire pour compenser les sous ou sur productions. Afin que ces procédés puissent être intégrés dans le processus d’équilibre offre-demande, ils sont regroupés au sein d’une centrale virtuelle d’agrégation de flexibilité, qui est vue alors comme une centrale virtuelle. Comme pour tout autre moyen de production du réseau, il est nécessaire de déterminer son plan de production. Nous proposons dans un premier temps dans cette thèse une architecture et un mode de gestion pour une centrale d’agrégation composée de n’importe quel type de procédés. Dans un second temps, nous présentons des algorithmes permettant de calculer le plan de production des différents types de procédés respectant toutes leurs contraintes de fonctionnement. Et enfin, nous proposons des approches pour calculer le plan de production de la centrale d’agrégation dans le but de maximiser son gain financier en respectant les contraintes réseau. / The desire to increase the share of renewable energies in the energy mix leads to an increase inshare of volatile and non-controllable energy and makes it difficult to meet the supply-demand balance. A solution to manage anyway theses energies in the current electrical grid is to deploy new energy storage and demand response systems across the country to counter balance under or over production. In order to integrate all these energies systems to the supply and demand balance process, there are gathered together within a virtual flexibility aggregation power plant which is then seen as a virtual power plant. As for any other power plant, it is necessary to compute its production plan. Firstly, we propose in this PhD thesis an architecture and management method for an aggregation power plant composed of any type of energies systems. Then, we propose algorithms to compute the production plan of any types of energy systems satisfying all theirs constraints. Finally, we propose an approach to compute the production plan of the aggregation power plant in order to maximize its financial profit while complying with all the constraints of the grid.

Dans cette thèse, on s'intéresse aux plus grands facteur premiers d'entiers consécutifs. Désignons par $P^+(n)$ (resp. $P^-(n)$) le plus grand (resp. plus petit) facteur premier d'un entier générique $n\geq 1$ avec la convention que $P^+(1)=1$ (resp. $P^-(1)=\infty$). Dans le premier chapitre, nous étudions les plus grands facteurs premiers d'entiers consécutifs dans les petits intervalles. Nous démontrons qu'il existe une proportion positive d'entiers $n$ tels que $P^+(n)<P^+(n+1)$ pour $n\in\, ]x,\, x+y]$ avec $y=x^{\theta}, \tfrac{7}{12}<\theta\leq 1$. Nous obtenons un résultat similaire pour la condition $P^+(n)>P^+(n+1)$. Dans le deuxième chapitre, nous nous intéressons à la fonction $P_y^+(n)$, où $P_y^+(n)=\max\{p|n:\, p\leq y\}$ et $2\leq y\leq x.$ Nous montrons qu'il existe une proportion positive d'entiers $n$ tels que $P_y^+(n)<P_y^+(n+1)$. En particulier, la proportion d'entiers $n$ avec $P^+(n)<P^+(n+1)$ est plus grande que $0,1356$ en prenant $y=x.$ Les outils principaux sont le crible et un système de poids bien adapté. Dans le troisième chapitre, nous démontrons que les deux configurations $P^+(n-1)>P^+(n)<P^+(n+1)$ et $P^+(n-1)<P^+(n)>P^+(n+1)$ ont lieu pour une proportion positive d'entiers $n$, en utilisant le système de poids bien adapté que l'on a introduit dans le Chapitre 2. De façon similaire, on peut obtenir un résultat plus général pour $k$ entiers consécutifs, $k\in \mathbb{Z}, k\geq3$. Dans le quatrième chapitre, on étudie les plus grands facteurs premiers d'entiers consécutifs voisins d'un entier criblé. Sous la conjecture d'Elliott-Halberstam, nous montrons d'abord que la proportion de la configuration $P^+(p-1)<P^+(p+1)$ est plus grande que $0,1779$. Puis, nous démontrons qu'il existe une proportion positive d'entiers $n$ tels que $P^+(n)<P^+(n+2), P^-(n)>x^{\beta}$ avec $0<\beta<\frac{1}{3}$ / In this thesis, we study the largest prime factors of consecutive integers. Denote by $P^+(n)$ (resp. $P^-(n)$) the largest (resp. the smallest) prime factors of the integer $n\geq 1$ with the convention $P^+(1)=1$ (resp. $P^-(1)=\infty$). In the first chapter, we consider the largest prime factors of consecutive integers in short intervals. We prove that there exists a positive proportion of integers $n$ for $n\in\, (x,\, x+y]$ with $y=x^{\theta}, \tfrac{7}{12}<\theta\leq 1$ such that $P^+(n)<P^+(n+1)$. A similar result holds for the condition $P^+(n)>P^+(n+1)$. In the second chapter, we consider the function $P_y^+(n)$, where $P_y^+(n)=\max\{p|n:\, p\leq y\}$ and $2\leq y\leq x$. We prove that there exists a positive proportion of integers $n$ such that $P_y^+(n)<P_y^+(n+1)$. In particular, the proportion of the pattern $P^+(n)<P^+(n+1)$ is larger than $0.1356$ by taking $y=x.$ The main tools are sieve methods and a well adapted system of weights. In the third chapter, we prove that the two patterns $P^+(n-1)>P^+(n)<P^+(n+1)$ and $P^+(n-1)<P^+(n)>P^+(n+1)$ occur for a positive proportion of integers $n$ respectively, by the well adapted system of weights that we have developed in the second chapter. With the same method, we derive a more general result for $k$ consecutive integers, $k\in \mathbb{Z}, k\geq 3$. In the fourth chapter, we study the largest prime factors of consecutive integers with one of which without small prime factor. Firstly we show that under the Elliott-Halberstam conjecture, the proportion of the pattern $P^+(p-1)<P^+(p+1)$ is larger than $0.1779$. Then, we prove that there exists a positive proportion of integers $n$ such that $P^+(n)<P^+(n+2), P^-(n)>x^{\beta}$ with $0<\beta<\frac{1}{3}$

Dans cette thèse, on étudie deux types d’équations diophantiennes. Une première partie de notre étude porte sur la résolution des équations dites de Ramanujan-Nagell Cx2+ b2mD = yn. Une deuxième partie porte sur les équations dites de Ngell-Ljunggren xp+ypx+y = pezq incluant le cas diagonal p = q. Les nouveaux réesultats obtenus seront appliqués aux équations de la forme xp + yp = Bzq. L’équation de Catalan-Fermat (cas B = 1) fera l’objet d’un traitement à part. / In this thesis, we study two types of diophantine equations. A ?rst part of our study is about the resolution of the Ramanujan-Nagell equations Cx2 + b2mD = yn. A second part of our study is about the Nagell-Ljungren equations xp+yp x+y = pezq including the diagonal case p = q. Our new results will be applied to the diophantine equations of the form xp + yp = Bzq. The Fermat-Catalan equation (case B = 1) will be the subject of a special study.

Cette thèse est consacrée à l’étude d’expansions de certaines structures algébriques et leur place dans la classification modèle-théorique des structures, initiée par Shelah. La première partie aborde de manière abstraite l’expansion d’une théorie par un prédicat aléatoire –ou générique– pour une sous-structure modèle d’un réduit de la théorie. Nous éla- borons un critère pour l’existence d’une telle expansion, qui est vérifié pour certaines théories de structures algébriques. En particulier, nous montrons l’existence de sous-groupes additifs génériques pour certaines théories de corps, ainsi que de sous-groupes multiplicatifs génériques pour les corps algébriquement clos en toute caractéristique. Nous étudions aussi la conservation de diverses notions de néostabilité, en particulier nous montrons que cette expansion préserve la propriété NSOP 1 , mais en général ne préserve pas la simplicité. Nous produisons par cette construction de nouveaux exemples de structures NSOP 1 non simples, et faisons une étude toute particulière de l’une d’entre elles : l’expansion d’un corps algébriquement clos de caractéristique positive par un sous-groupe additif générique. La deuxième partie étudie les expansions du groupe des entiers par des valuations p-adiques. Nous montrons l’élimination des quantificateurs dans un langage naturel et calculons le dp-rang d’une telle expansion : il est égal au nombre de valuations considérées. L’expansion du groupe des entiers par une seule valuation p-adique est donc une nouvelle expansion dp-minimale du groupe des entiers. Enfin, nous montrons que cette dernière n’admet pas de structures intermédiaires : tout ensemble définissable dans l’expansion est soit définissable dans le groupe des entiers, soit capable de “reconstruire” la valuation en utilisant seulement la structure additive / This thesis is concerned with the expansions of some algebraic structures and their fit in Shelah’s classification landscape. The first part deals with the expansion of a theory by a random –or generic– predicate for a substructure model of a reduct of the theory. We describe a setup allowing such an expansion to exist, which is suitable for several algebraic structures. In particular, we obtain the existence of additive generic subgroups of some theories of fields and multiplicative generic subgroups of algebraically closed fields in all characteristic. We also study the preservation of certain neostability notions, for instance, the NSOP 1 property is preserved but the simplicity is not in general. Thus, this construction produces new examples of NSOP 1 not simple theories, and we study in depth a particular example: the expansion of an algebraically closed field of positive characteristic by a generic additive subgroup. The second part studies expansions of the groups of integers by p-adic valuations. We prove quantifier elimination in a natural language and compute the dp-rank of these expansions: it equals the number of distinct p-adic valuations considered. Thus, the expansion of the integers by one p-adic valuation is a new dp-minimal expansion of the group of integers. Finally, we prove that the latter expansion does not admit intermediate structures: any definable set in the expansion is either definable in the group structure or is able to "reconstruct" the valuation using only the group operation

Mes travaux de recherche portent sur la théorie de la démonstration, le lambda-calcul et l'informatique théorique, dans la ligne de la correspondance de Curry-Howard entre les preuves et les programmes.<br /><br />Dans ma thèse de doctorat, j'ai étudié les opérateurs de mise en mémoire pour les types de données. Ces notions, qui sont introduites par Krivine, permettent de programmer en appel par valeur tout en utilisant la stratégie de la réduction de tête pour exécuter les $\lambda$-termes. Pour cette étude, j'ai introduit avec David une extension du $\lambda$-calcul avec substitutions explicites appelée $\lambda$-calcul dirigé. Nous en avons déduit une nouvelle caractérisation des termes de mise en mémoire et obtenu des nombreux résultats très fins à leur sujet. En ce qui concerne le typage des opérateurs de mise en mémoire, Krivine a trouvé une formule du second ordre, utilisant la non-non traduction de Gödel de la logique classique dans la logique intuitionniste, qui caractérise ces opérateurs. Je me suis attaché à diverses généralisations du résultat de Krivine pour les types à quantificateur positif dans des extensions de la logique des prédicats du second ordre.<br /><br />J'ai poursuivi, après ma thèse, une activité de recherche sur l'extension de la correspondance de Curry-Howard à la logique classique, au moyen des instructions de contrôle. J'ai étudié des problèmes liés aux types de données dans deux de ces systèmes : le $\lambda \mu$-calcul de Parigot et le $\lambda C$-calcul de Krivine. J'ai donné des algorithmes très simples permettant de calculer la valeur d'un entier classique dans ces deux systèmes. J'ai également caractérisé les termes dont le type est l'une des règles de l'absurde. J'ai étendu le système de Parigot pour en obtenir une version non déterministe mais où les entiers se réduisent toujours en entiers de Church. Curieusement, ce système permet de programmer la fonction ``ou parallèle''.<br /><br />Je me suis intéressé aux systèmes numériques qui servent à représenter les entiers naturels au sein du $\lambda$-calcul. J'ai montré que pour un tel système, la possession d'un successeur, d'un prédécesseur et d'un test à zéro sont des propriétés indépendantes, puis qu'un système ayant ces trois fonctions possède toujours un opérateur de mise en mémoire. Dans un cadre typé, j'ai apporté une réponse négative à une conjecture de Tronci qui énonçait une réciproque du résultat précédent.<br /><br />La notion de mise en mémoire ne s'applique qu'à des types de données. Une définition syntaxique a été donné par Böhm et Berarducci, et Krivine a proposé une définition sémantique de ces types. J'ai obtenu avec Farkh des résultats reliant la syntaxe et la sémantique des types de données. Nous avons proposé également des définitions des types entrée et des types sortie pour lesquelles nous avons montré diverses propriétés syntaxiques et sémantiques.<br /><br />J'ai réussi à combiner la logique intuitionniste et la logique classique en une logique mixte. Dans cette logique, on distingue deux genres de variables du second ordre, suivant que l'on peut, ou non, leur appliquer le raisonnement par l'absurde. Ce cadre m'a permi de donner le type le plus général pour les opérateurs de mise en mémoire. Vu le rôle important que cette logique semble devoir jouer dans la théorie de ces opérateurs, j'en ai mené avec A. Nour une étude théorique approfondie. Le système de logique mixte propositionnelle auquelle nous avons abouti évoque les sytèmes $LC$ de Girard et $LK^{tq}$ de Danos, Joinet et Schellinx.<br /><br />Je me suis intéressé avec David à l'équivalence induite par l'égalité entre les arbres de Böhm infiniment $\eta$-expansés. Avec Raffalli, je me suis également intéressé à la sémantique de la logique du second ordre.

Les études menées permettent d’étendre la méthodologie de commande H∞ aux modèles décrits par des équations différentielles faisant intervenir des ordres de dérivation non entiers. Deux approches sont proposées. La première consiste à réécrire le modèle non entier comme un modèle entier incertain afin de pouvoir utiliser les méthodes de commande H∞ développées pour les modèles entiers. La seconde approche consiste à développer des conditions LMI spécifiques aux modèles non entiers à partir de leur pseudo représentation d’état. Ces deux approches sont appliquées à l’isolation vibratoire d’un pont. / The general theme of the work enables to extend H∞ control methodology to fractional order models. Two approaches are proposed. The first one consists in rewriting the fractional order model as an uncertain integer order model in order to use existing H∞ control methods for integer order models. The second approach consists in developing specific LMI conditions for fractional order models based on their pseudo state space representation. These two approaches are applied to the vibratory isolation of a bridge.

Selon le rapport annuel de la croix rouge et du croissant rouge pour l’année 2006, le nombre de catastrophes, d’origine naturelle et humaine, a augmenté ces dernières décennies dans des proportions importantes. Ces catastrophes engendrent souvent un nombre de victimes important nécessitant des interventions urgentes. Face à une telle situation, les moyens sanitaires classiques et de routines se trouvent souvent dépassés, et par conséquent inefficaces pour absorber cet afflux massif de victimes. Ainsi, la mise en œuvre d’un système de gestion hospitalier conditionné par une optimisation des différentes ressources médicales est indispensable pour sauver le maximum de vies humaines. Dans ce contexte, nous proposons dans cette thèse, d’étudier le problème d’optimisation des ressources humaines et matérielles critiques à savoir, les chirurgiens et les salles opératoires en situation de crise. L’objectif est de traiter le maximum de victimes, autrement dit sauver le maximum de vies humaines. Notre étude comprend deux niveaux : (1) un niveau préparatoire qui consiste à dimensionner les ressources dans le cadre des exercices de simulation du plan blanc, et (2) un niveau opérationnel permettant d’optimiser l’ordonnancement des interventions dans les salles opératoires. Aussi, nous étudions l’impact de la mutualisation des ressources sur le nombre de victimes traitées. L’un des défis posés à la programmation opératoire en situation d’exception est l’aptitude à faire face aux perturbations. Dans ce cadre, nous abordons le problème réactif d’optimisation de l’ordonnancement des interventions dans les salles opératoires. Nous considérons diverses perturbations possibles telles : une durée opératoire qui dépasse la durée estimée, l’insertion d’une nouvelle victime dans le programme opératoire, et l’évolution du degré d’urgence d’une victime. Cette thèse est menée avec la collaboration de plusieurs structures sanitaires publiques en France et en Tunisie. Les résultats expérimentaux mettent en exergue l’apport de ces approches pour l’aide à la décision. / Disaster like terrorist attack, earthquake, and hurricane, often cause a high degree of damage. Thousands of people might be affected. The 2006’s annual report of the International Federation of Red Cross and Red Crescent Societies proves that the number of disasters increased during these last decades. In such situations, hospitals must be able to receive injured persons for medical and surgical treatments. For these reasons medical resources optimization of different is fundamental in human life save.In this context, we propose in this thesis, to study the optimization of human and material resources in relation with hospital management. We focus more precisely on critical resources: operating rooms and surgeons. The goal is to handle the maximum of victims and then to save the maximum of human lives. Our research consists of two phases: (1) Sizing critical resources during the preparedness phase of disaster management plan so called white plan. (2) Operational phase that provides the optimization of surgical acts scheduling in the operating rooms. Also, we study the impact of sharing resources on the number of treated victims. A disaster situation is characterized by different disruptions. In this setting, we approach a reactive problem for optimization of surgical acts scheduling in the operating rooms. We consider various possible disruptions: the overflow of assessed surgical care duration, the insertion of a new victim in the scheduling program, and the evolution of victim’s emergency level.This work is achieved with the collaboration of several public health institutions (hospitals, ministry, etc.) both in France and Tunisia. Empirical study shows that a substantial aid is proposed by using the proposed approaches.

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.