Les systèmes critiques comme les commandes de vol peuvent entraîner des désastres en cas de dysfonctionnement. D'où l'intérêt porté à la fois par le monde industriel et académique aux méthodes de preuve formelle capable d'apporter, plus ou moins automatiquement, une preuve mathématique de correction. Parmi elles, cette thèse s'intéresse particulièrement à l'interprétation abstraite, une méthode efficacepour générer automatiquement des preuves de propriétés numériques qui sont essentielles dans notre contexte.Il est bien connu des automaticiens que les contrôleurs linéaires sont stables si et seulement si ils admettent un invariant quadratique(un ellipsoïde, d'un point de vue géométrique). Ils les appellent fonction de Lyapunov quadratique et une première partie propose d'encalculer automatiquement pour des contrôleurs donnés comme paire de matrices. Ceci est réalisé en utilisant des outils de programmation semi-définie. Les aspects virgule flottante sont pris en compte, que ce soit dans les calculs effectués par le programme analysé ou dans les outils utilisés pour l'analyse. Toutefois, le véritable but est d'analyser des programmes implémentant des contrôleurs (et non des paires de matrices), incluant éventuellement des réinitialisation ou des saturations, donc non purement linéaires. L'itération sur les stratégies est une techniqued'analyse statique récemment développée et bien adaptée à nos besoins. Toutefois, elle ne se marrie pas facilement avec lestechniques classiques d'interprétation abstraite. La partie suivante propose une interface entre les deux mondes.Enfin, la dernière partie est un travail plus préliminaire sur l'usage de l'optimisation globale sur des polynômes basée sur les polynômes deBernstein pour calculer des invariants polynomiaux sur des programmes polynomiaux. / Critical Systems such as flight commands may have disastrous results in case of failure. Hence the interest of both the industrial and theacademic communities in formal methods able to more or less automatically deliver mathematical proof of correctness. Among them, this thesis will particularly focus on abstract interpretation, an efficient method to automatically generate proofs of numerical properties which are essential in our context.It is well known from control theorists that linear controllers are stable if and only if they admit a quadratic invariant (geometrically speaking, an ellipsoid). They call these invariants quadratic Lyapunov functions and a first part offers to automatically compute such invariants for controllers given as a pair of matrices. This is done using semi-definite programming optimization tools. It is worth noting that floating point aspects are taken care of, whether they affectcomputations performed by the analyzed program or by the tools used for the analysis.However, the actual goal is to analyze programs implementing controllers (and not pairs of matrices), potentially including resets or saturations, hence not purely linears. The policy iteration technique is a recently developed static analysis techniques well suited to that purpose. However, it does not marry very easily with the classic abstract interpretation paradigm. The next part tries to offer a nice interface between the two worlds.Finally, the last part is a more prospective work on the use of polynomial global optimization based on Bernstein polynomials to compute polynomial invariants on polynomials systems.

La thèse présente une étude numérique des instabilités de trajectoires de sphères, d'ellipsoïdes aplatis et de bulles en mouvement libre sous l'action de la gravité, de la poussée d'Archimède et des forces hydrodynamiques. Le chapitre sur les sphères reprend, complète et étend l'étude numérique de Jenny et al. (2004) en se concentrant sur la transition au chaos et sur les trajectoires chaotiques. Les résultats montrent la différence entre le scénario de transition au chaos de sphères de faible et de grand rapport de densité. Plusieurs grandeurs statistiques sont proposées afin de fournir une caractérisation quantitative des états chaotiques. Elle permettent de mettre en relation les états ordonnées et chaotiques et offrent une possibilité de comparaison objective de données aléatoires d'origine numérique ou expérimentale. L'étude, très extensive, du comportement d'ellipsoïdes aplatis établit le lien entre les disques et les sphères en faisant varier l'aplatissement des objets depuis infiniment plat jusqu'à presque sphérique. Les huit diagrammes d'état présentés permettent de comprendre l'effet de la forme des ellipsoïdes sur le scénario de transition. Le cas d'ellipsoïdes presque sphériques montre que de faibles imperfections de la forme peuvent avoir in impact significatif sur les trajectoires de sphères de très faible rapport de densité. Pour les bulles considérées dans la limite de rapport de densité et viscosité az/liquide nul, l'étude se concentre sur l'analyse de stabilité linéaire et aboutit à la courbe de stabilité marginale dans le plan des paramètres nombre de Bond – nombre de Galilée en tenant compte de la déformation des bulles au moment de la perte de leur axisymétrie. Plus deux décades de nombres de Bond, entre 0,1 et 20, sont couvertes. Les résultats montrent clairement l'effet de la déformation de la bulle sur le seuil de l'instabilité. / The thesis presents a numerical study of path instabilities for spheres, oblate spheroids and bubbles moving freely under the effect of the gravity, buoyancy and hydrodynamic forces. For spheres, the parametric study of Jenny et al. (2004) is revisited, improved end extended with a special focus on the chaotic states. The results reveal that the effect of density ratio responsible for different oblique oscillating states of low and high frequencies has a significant impact both on the onset of chaos and on the behavior of fully chaotic states. Several quantitative statistical quantities are proposed and shown to be relevant for establishing the relation between chaotic and ordered states and for an objective comparison of random data of numerical or experimental origin. The extensive study on freely moving spheroids establishes the link between disks and spheres by varying the aspect ratio of spheroids from infinitely flat to almost spherical. The state diagrams provided for eight different aspect ratios of spheroid show in detail how the transition scenario varies depending of the body shape. The investigation of almost spherical spheroids reveals the specificities of the dynamics of light imperfect spheres.For the deformable gas bubble in the limit of zero gas/liquid density and viscosity ratio, a marginal stability curve is given in the two-parameter plane of the Galileo and the Bond number indicating the critical Galileo numbers for the loss of stability of vertical trajectories. The numerical investigation covers more than two decades of Bond number going from 0.1 to 20. The results clearly show the crucial role of the surface deformation.