Cette thèse se positionne dans le domaine de la vérification déductive de programmes, qui consiste à transformer une propriété à vérifier sur un programme en un énoncé logique, pour ensuite démontrer cet énoncé. La vérification effective d'un programme peut poser de nombreuses difficultés pratiques. En fait, les concepts mis en jeu derrière le programme peuvent suffire à faire obstacle à la vérification. En effet, certains programmes peuvent être assez courts et n'utiliser que des constructions simples, et pourtant s'avérer très difficiles à vérifier. Cela nous amène à la question suivante: dans le contexte d'un environnement de vérification déductive de programmes basé sur les démonstrateurs automatiques, quelles méthodes appliquer pour réduire l'effort nécessaire à la fois pour spécifier des comportements attendus complexes, ainsi que pour démontrer qu'un programme respecte ces comportements attendus? Pour mener notre étude, nous nous sommes placés dans le cadre de l'environnement de vérification déductive de programmes Why3. La vérification de programmes en Why3 est basée sur la génération de conditions de vérification, et l'usage de démonstrateurs externes pour les prouver, que ces démonstrateurs soient automatiques ou interactifs. Nous avons développé plusieurs méthodes, certaines générales et d'autres spécifiques à des classes de programmes, pour réduire l'effort manuel. Nos contributions sont les suivantes. Tout d'abord, nous ajoutons des fonctionnalités à Why3 pour assister le processus de vérification, notamment un mécanisme léger de preuve déclarative basé sur la notion d'indicateurs de coupures. Ensuite, nous présentons une méthode de vérification d'absence de débordement arithmétique pour une classe d'utilisation des entiers difficile à traiter par les méthodes standards. Enfin, nous nous intéressons au développement d'une bibliothèque générique pour la spécification et la preuve de programmes générateurs de code. / This thesis is set in the domain of deductive verification of programs, which consists of transforming a property to be verified about a program into a logical statement, and then proving this statement. Effective verification of a program can pose many practical difficulties. In fact, the concepts behind the program may be sufficient to impede verification. Indeed, some programs can be quite short and use only simple constructions, and yet prove very difficult to verify. This leads us to the following question: in the context of a deductive program verification environment based on automatic provers, what methods can be applied to reduce the effort required both to specify complex behaviors, as well as to prove that a program respects these expected behaviors? To carry out our study, we placed ourselves in the context of the deductive verification environment of programs Why3. The verification of programs in Why3 is based on the generation of verification conditions, and the use of external provers to prove them, whether these provers are automatic or interactive. We have developed several methods, some general and others specific to some program classes, to reduce manual effort. Our contributions are as follows. First, we add features to Why3 to assist the verification process, including a lightweight declarative proof mechanism based on the notion of cut indicators. Then we present a method for checking the absence of arithmetic overflow, for use cases which are difficult to process by standard methods. Finally, we are interested in the development of a generic library for the specification and proof of code generating programs.

Many partial differential equations (PDEs) admit conserved quantities like mass or energy. Those quantities are often essential to establish well-posed results. When approximating a PDE by a finite-difference scheme, it is natural to ask whether related discretized quantities remain conserved under the scheme. Such conservation may establish the stability of the numerical scheme. We present an algorithm for checking the preservation of a polynomial quantity under a polynomial finite-difference scheme. In our algorithm, schemes can be explicit or implicit, have higher-order time and space derivatives, and an arbitrary number of variables. Additionally, we present an algorithm for, given a scheme, finding conserved quantities. We illustrate our algorithm by studying several finite-difference schemes.

L'autonomie est l'une des préoccupations majeures lors du développement de missions spatiales que l'objectif soit scientifique (exploration interplanétaire, observations, etc) ou commercial (service en orbite). Pour le rendez-vous spatial, cette autonomie dépend de la capacité embarquée de contrôle du mouvement relatif entre deux véhicules spatiaux. Dans le contexte du service aux satellites (dépannage, remplissage additionnel d'ergols, correction d'orbite, désorbitation en fin de vie, etc), la faisabilité de telles missions est aussi fortement liée à la capacité des algorithmes de guidage et contrôle à prendre en compte l'ensemble des contraintes opérationnelles (par exemple, saturation des propulseurs ou restrictions sur le positionnement relatif entre les véhicules) tout en maximisant la durée de vie du véhicule (minimisation de la consommation d'ergols). La littérature montre que ce problème a été étudié intensément depuis le début des années 2000. Les algorithmes proposés ne sont pas tout à fait satisfaisants. Quelques approches, par exemple, dégradent les contraintes afin de pouvoir fonder l'algorithme de contrôle sur un problème d'optimisation efficace. D'autres méthodes, si elles prennent en compte l'ensemble du problème, se montrent trop lourdes pour être embarquées sur de véritables calculateurs existants dans les vaisseaux spatiaux. Le principal objectif de cette thèse est le développement de nouveaux algorithmes efficaces et validés pour le guidage et le contrôle impulsif des engins spatiaux dans le contexte des phases dites de "hovering" du rendez-vous orbital, i.e. les étapes dans lesquelles un vaisseau secondaire doit maintenir sa position à l'intérieur d'une zone délimitée de l'espace relativement à un autre vaisseau principal. La première contribution présentée dans ce manuscrit utilise une nouvelle formulation mathématique des contraintes d'espace pour le mouvement relatif entre vaisseaux spatiaux pour la conception d'algorithmes de contrôle ayant un traitement calculatoire plus efficace comparativement aux approches traditionnelles. La deuxième et principale contribution est une stratégie de contrôle prédictif qui assure la convergence des trajectoires relatives vers la zone de "hovering", même en présence de perturbations ou de saturation des actionneurs. [...] / Autonomy is one of the major concerns during the planning of a space mission, whether its objective is scientific (interplanetary exploration, observations, etc.) or commercial (service in orbit). For space rendezvous, this autonomy depends on the on-board capacity of controlling the relative movement between two spacecraft. In the context of satellite servicing (troubleshooting, propellant refueling, orbit correction, end-of-life deorbit, etc.), the feasibility of such missions is also strongly linked to the ability of the guidance and control algorithms to account for all operational constraints (for example, thruster saturation or restrictions on the relative positioning between the vehicles) while maximizing the life of the vehicle (minimizing propellant consumption). The literature shows that this problem has been intensively studied since the early 2000s. However, the proposed algorithms are not entirely satisfactory. Some approaches, for example, degrade the constraints in order to be able to base the control algorithm on an efficient optimization problem. Other methods accounting for the whole set of constraints of the problem are too cumbersome to be embedded on real computers existing in the spaceships. The main object of this thesis is the development of new efficient and validated algorithms for the impulsive guidance and control of spacecraft in the context of the so-called "hovering" phases of the orbital rendezvous, i.e. the stages in which a secondary vessel must maintain its position within a bounded area of space relatively to another main vessel. The first contribution presented in this manuscript uses a new mathematical formulation of the space constraints for the relative motion between spacecraft for the design of control algorithms with more efficient computational processing compared to traditional approaches. The second and main contribution is a predictive control strategy that has been formally demonstrated to ensure the convergence of relative trajectories towards the "hovering" zone, even in the presence of disturbances or saturation of the actuators.[...]

In partial differential equations (PDEs), conserved quantities like mass and momentum are fundamental to understanding the behavior of the described physical systems. The preservation of conserved quantities is essential when using numerical schemes to approximate solutions of corresponding PDEs. If the discrete solutions obtained through these schemes fail to preserve the conserved quantities, they may be physically meaningless and unreliable. Previous approaches focused on checking conservation in PDEs and numerical schemes, but they did not give adequate attention to systematically handling parameters. This is a crucial aspect because many PDEs and numerical schemes have parameters that need to be dealt with systematically. Here, we investigate if the discrete analog of a conserved quantity is preserved under the solution induced by a parametric finite difference method. In this thesis, we modify and enhance a pre-existing algorithm to effectively and reliably deduce conserved quantities in the context of parametric schemes, using the concept of comprehensive Groebner systems. The main contribution of this work is the development of a versatile algorithm capable of handling various parametric explicit and implicit schemes, higher-order derivatives, and multiple spatial dimensions. The algorithm’s effectiveness and efficiency are demonstrated through examples and applications. In particular, we illustrate the process of selecting an appropriate numerical scheme among a family of potential discretization for a given PDE.