Depuis l'apparition des premiers ordinateurs, l'arithmétique flottante a énormément évolué. La norme IEEE 754 a permis de fixer les caractéristiques de l'arithmétique des ordinateurs modernes, mais les scientifiques perdent de plus en plus vite le contrôle de la validité de leurs calculs. Malgré l'énorme travail associé à la définition des opérations, la validation des calculs ne peut toujours pas être assurée de façon certaine par l'arithmétique implantée sur les ordinateurs. Je présente dans la première partie de cette étude deux prolongements qui visent à augmenter la marge de validité des opérations : un nouveau mode d'arrondi pour les fonctions trigonométriques et un codage efficace des intervalles accessible facilement à l'utilisateur. Je présente aussi dans cette partie une étude détaillée de la fonction unit in the last place et la probabilité d'absorption ou de propagation des erreurs dans une chaîne de multiplication. Ces travaux, qui viennent s'ajouter aux travaux antérieurs d'autres équipes de recherche et aux solutions que j'ai proposées dans ma thèse de master montrent les bénéfices que l'on pourra tirer des deux extensions présentées. L'arithmétique en-ligne permet de gérer efficacement les problèmes de précision, mais les opérateurs élémentaires utilisés sont peu adaptés aux architectures modernes de 32 ou 64 bits. L'implantation efficace d'un opérateur en-ligne ne peut que passer par la description d'un circuit de bas niveau. Les prédiffusés actifs, terme français utilisé pour Field Programmable Gate Array, sont des composants spéciaux programmables au niveau des portes logiques. Ils permettent d'abaisser les coûts de production en évitant de fabriquer un prototype. Nous avons implanté grâce à ces technologies les opérateurs simples de calcul en-ligne : addition, normalisation, etc...Le Noyau Arithmétique de Calcul En-Ligne (Nacel) décrit dans ce mémoire permet d'implanter les opérations arithmétiques usuelles telles que la multiplication, la division, l'extraction de racine carrée et les fonctions élémentaires trigonométriques et hyperboliques par une approximation polynômiale. Les architectures à flots de données sont insensibles aux difficultés sur lesquelles butent les concepteurs des ordinateurs modernes : temps d'accès à la mémoire, latence de communication, occupation partielle du pipeline d'instructions. Je décris dans ce document le mode de fonctionnement d'une machine virtuelle appelée Petite Unité de Calcul En-ligne (Puce). Par une gestion adaptée des étiquettes inspirée pour le contrôle des données de celle utilisée par la Manchester Data Flow Machine, Puce reproduit le comportement complet d'une machine à flot de données. Elle comprend de plus les opérations en-ligne de calcul scientifique. Nous présentons afin de valider le modèle d'évaluation de Puce les résultats de simulations logicielles pour une ou plusieurs unités fonctionnelles.

Le sujet de cette thèse est le développement de méthodes pour la découverte automatique des propriétés des variables numériques d'un programme. Nous nous plaçons dans le cadre de l'interprétation abstraite et introduisons plusieurs nouveaux domaines numériques, dont celui des octogones, de coût et de précision intermédiaires entre les domaines non relationnels (peu précis) et relationnels (coûteux) existants. Nous présentons leur adaptation à l'analyse des nombres à virgule flottante, jusqu'à présent limitée aux domaines non relationnels. Enfin, nous présentons les méthodes génériques de linéarisation et de propagation symbolique améliorant leur précision pour un surcoût réduit. Les méthodes introduites dans cette thèse ont été intégr! ées à l'analyseur Astrée et appliquées à la preuve d'absence d'erreurs dans le logiciel embarqué critique de commande de vol des avions Airbus A340, justifiant ainsi l'intérêt de nos méthodes pour des cadres d'applications réelles.

Les limites physiques des circuits à base de silicium étant en passe d'être atteintes, de nouveaux moyens doivent être trouvés pour outrepasser la fin de la loi de Moore. Beaucoup d'applications peuvent tolérer des approximations dans leurs calculs à différents niveaux, sans dégrader la qualité de leur sortie, ou en la dégradant de manière acceptable. Cette thèse se concentre sur les architectures arithmétiques approximatives afin de saisir cette opportunité. Tout d'abord, une étude critique de l'état de l'art des additionneurs et multiplieurs approximatifs est présentée. Ensuite, un modèle de propagation d'erreur virgule-fixe mettant en œuvre la densité spectrale de puissance est proposée, suivi d'un modèle de propagation du taux d'erreur binaire positionnel des opérateurs approximatifs. Les opérateurs approximatifs sont ensuite utilisés pour la reproduction des effets de la VOS dans les opérateurs arithmétiques exacts. Grâce à notre outil de travail open-source ApxPerf et ses bibliothèques synthétisables C++ apx_fixed pour les opérateurs approximatifs et ct_float pour l'arithmétique flottante basse consommation, deux études consécutives sont proposées, basées sur des applications de traitement du signal complexes. Tout d'abord, les opérateurs approximatifs sont comparés à l'arithmétique virgule-fixe, et la supériorité de la virgule-fixe est soulignée. Enfin, la virgule fixe est comparée aux petits flottants dans des conditions équivalentes. En fonction des conditions applicatives, la virgule-flottante montre une compétitivité inattendue face à la virgule-fixe. Les résultats et discussions de cette thèse donnent un regard nouveau sur l'arithmétique approximative et suggère de nouvelles directions pour le futur des architectures efficaces en énergie. / The physical limits being reached in silicon-based computing, new ways have to be found to overcome the predicted end of Moore's law. Many applications can tolerate approximations in their computations at several levels without degrading the quality of their output, or degrading it in an acceptable way. This thesis focuses on approximate arithmetic architectures to seize this opportunity. Firstly, a critical study of state-of-the-art approximate adders and multipliers is presented. Then, a model for fixed-point error propagation leveraging power spectral density is proposed, followed by a model for bitwise-error rate propagation of approximate operators. Approximate operators are then used for the reproduction of voltage over-scaling effects in exact arithmetic operators. Leveraging our open-source framework ApxPerf and its synthesizable template-based C++ libraries apx_fixed for approximate operators, and ct_float for low-power floating-point arithmetic, two consecutive studies are proposed leveraging complex signal processing applications. Firstly, approximate operators are compared to fixed-point arithmetic, and the superiority of fixed-point is highlighted. Secondly, fixed-point is compared to small-width floating-point in equivalent conditions. Depending on the applicative conditions, floating-point shows an unexpected competitiveness compared to fixed-point. The results and discussions of this thesis give a fresh look on approximate arithmetic and suggest new directions for the future of energy-efficient architectures.

Cette thèse fait une étude sur deux moyens d'enrichir l'environnement flottant courant : le premier est d'obtenir plusieurs versions d'implantation pour chaque fonction mathématique, le deuxième est de fournir des opérations de la norme IEEE754, qui permettent de mélanger les entrées et la sortie dans les bases différentes. Comme la quantité de versions différentes pour chaque fonction mathématique est énorme, ce travail se concentre sur la génération du code. Notre générateur de code adresse une large variété de fonctions: il produit les implantations paramétrées pour les fonctions définies par l'utilisateur. Il peut être vu comme un générateur de fonctions boîtes-noires. Ce travail inclut un nouvel algorithme pour le découpage de domaine et une tentative de remplacer les branchements pendant la reconstruction par un polynôme. Le nouveau découpage de domaines produit moins de sous-domaines et les degrés polynomiaux sur les sous-domaines adjacents ne varient pas beaucoup. Pour fournir les implantations vectorisables il faut éviter les branchements if-else pendant la reconstruction. Depuis la révision de la norme IEEE754 en 2008, il est devenu possible de mélanger des nombres de différentes précisions dans une opération. Par contre, il n'y a aucun mécanisme qui permettrait de mélanger les nombres dans des bases différentes dans une opération. La recherche dans l'arithmétique en base mixte a commencé par les pires cas pour le FMA. Un nouvel algorithme pour convertir une suite de caractères décimaux du longueur arbitraire en nombre flottant binaire est présenté. Il est indépendant du mode d'arrondi actuel et produit un résultat correctement arrondi. / This work investigates two ways of enlarging the current floating-point environment. The first is to support several implementation versions of each mathematical function (elementary such as $\exp$ or $\log$ and special such as $\erf$ or $\Gamma$), the second one is to provide IEEE754 operations that mix the inputs and the output of different \radixes. As the number of various implementations for each mathematical function is large, this work is focused on code generation. Our code generator supports the huge variety of functions: it generates parametrized implementations for the user-specified functions. So it may be considered as a black-box function generator. This work contains a novel algorithm for domain splitting and an approach to replace branching on reconstruction by a polynomial. This new domain splitting algorithm produces less subdomains and the polynomial degrees on adjacent subdomains do not change much. To produce vectorizable implementations, if-else statements on the reconstruction step have to be avoided. Since the revision of the IEEE754 Standard in 2008 it is possible to mix numbers of different precisions in one operation. However, there is no mechanism that allows users to mix numbers of different radices in one operation. This research starts an examination ofmixed-radix arithmetic with the worst cases search for FMA. A novel algorithm to convert a decimal character sequence of arbitrary length to a binary floating-point number is presented. It is independent of currently-set rounding mode and produces correctly-rounded results.

Les mémoires à nanocristaux de silicium sont considérées comme l'une des solutions les plus intéressantes pour remplacer les grilles flottantes dans les mémoires Flash pour des applications de mémoires non-volatiles embarquées. Ces nanocristaux sont intéressants pour leur compatibilité avec les technologies de procédé CMOS, et la réduction des coûts de fabrication. De plus, la taille des nanocristaux garantie un faible couplage entre les cellules et la robustesse contre les effets de SILC. L'un des principaux challenges pour les mémoires embarquées dans des applications mobiles et sans contact est l'amélioration de la consommation d'énergie afin de réduire les contraintes de design de cellules. Dans cette étude, nous présentons l'état de l'art des mémoires Flash à grille flottante et à nanocristaux de silicium. Sur ce dernier type de mémoire une optimisation des principaux paramètres technologiques a été effectuée pour permettre l'obtention d'une fenêtre de programmation compatible avec les applications à faible consommation d'énergie. L'étude s'attache à l'optimisation de la fiabilité de la cellule à nanocristaux de silicium. On présente pour la première fois une cellule fonctionnelle après un million de cycles d'écriture et effacement dans une large gamme de températures [-40°C;150°C], et qui est capable de retenir l'information pendant dix ans à 150°C. Enfin, une analyse de la consommation de courant et d'énergie durant la programmation montre l'adaptabilité de la cellule pour des applications à faible consommation. Toutes les données expérimentales ont été comparées avec les résultats d'une cellule standard à grille flottante pour montrer les améliorations apportées. / The silicon nanocrystal memories are one of the most attractive solutions to replace the Flash floating gate for nonvolatile memory embedded applications, especially for their high compatibility with CMOS process and the lower manufacturing cost. Moreover, the nanocrystal size guarantees a weak device-to-device coupling in an array configuration and, in addition, for this technology it has been shown the robustness against SILC. One of the main challenges for embedded memories in portable and contactless applications is to improve the energy consumption in order to reduce the design constraints. Today the application request is to use the Flash memories with both low voltage biases and fast programming operation. In this study, we present the state of the art of Flash floating gate memory cell and silicon nanocrystal memories. Concerning this latter device, we studied the effect of main technological parameters in order to optimize the cell performance. The aim was to achieve a satisfactory programming window for low energy applications. Furthermore, the silicon nanocrystal cell reliability has been investigated. We present for the first time a silicon nanocrystal memory cell with a good functioning after one million write/erase cycles, working on a wide range of temperature [-40°C; 150°C]. Moreover, ten years data retention at 150°C is extrapolated. Finally, the analysis concerning the current and energy consumption during the programming operation shows the opportunity to use the silicon nanocrystal cell for low power applications. All the experimental data have been compared with the results achieved on Flash floating gate memory, to show the performance improvement.

Suite à la mise en place de politiques publiques favorisant les énergies renouvelables, la construction de fermes éoliennes offshore est en plein essor aux quatre coins du monde. Or, la technique de l'éolienne offshore posée, la seule utilisée actuellement, n'est pas viable économiquement dans des eaux trop profondes. Ceci représente un sérieux frein au développement de l'énergie éolienne. Pour cette raison, la communauté scientifique s'intéresse depuis plusieurs années aux éoliennes sur plates-formes flottantes. En eau profonde, cette technologie est intéressante. Mais le fait que l'éolienne ne soit pas encastrée au fond de la mer augmente très significativement les sollicitations mécaniques induites par les vagues.Pour réduire ces sollicitations qui ont de nombreux effets néfastes, différentes approches sont possibles. Essayer de compenser les oscillations « avant-arrière » du mât de l'éolienne en pilotant la force de poussée exercée au niveau du rotor a déjà été écarté dans la littérature. Nous nous sommes concentrés sur l'ajout d'un dispositif de stabilisation interne à la plate-forme, de type Tuned Liquid Column Damper (un tube en U contenant un liquide, TLCD, encore appelé tube anti-roulis), utilisé dans d'autres contextes. Le dispositif que nous proposons est un dispositif actif où les paramètres du TLCD sont ajustés en temps réel, au cours du mouvement induit par les vagues. La mise à jour des paramètres suit une stratégie reposant sur une analyse des interactions entre le TLCD et la plate-forme (appelée ici barge) sur laquelle est installée l'éolienne. Nous avons modélisé le mouvement de la barge seul et son couplage avec le TLCD dans le plan grâce à une approche Lagrangienne. Nous avons étudié les effets des interactions du TLCD avec la barge dans le cas où le coefficient de perte de charge dans le tube était constant. Les limites de cette approche ont été détaillées grâce aux résultats classiques de la littérature sur les oscillateurs mécaniques couplés. Nous nous sommes ensuite concentrés sur une approche active consistant à modifier les caractéristiques du système en temps réel. Nous avons proposé des stratégies de type Linear Quadratic Regulator et de type Model Predictive Control agissant sur le coefficient de perte de charge. Dans un deuxième temps, les simulations nous ont ensuite permis d'écarter la commande MPC dont le rapport performance / complexité n'est pas favorable par rapport à la commande LQR dans ce cas précis.Une étude plus générale du système, en trois dimensions, nous a permis de vérifier que le TLCD classique dans sa version passive ou dans la version active que nous proposions n'est pas du tout robuste à l'incidence de la houle. Nous avons donc imaginé et modélisé des dispositifs inspirés du TLCD mais permettant d'amortir les oscillations de la houle de manière efficace, indépendamment de l'incidence de la houle. Nous avons nommé ces dispositifs TLMCD, pour Tuned Liquid Multiple Columns Damper.Les dispositif que nous proposons sont des systèmes TLMCD actifs. Ils sont conçus d'après les modélisations 3D que nous avons développées et une étude des coûts. Pour ces dispositifs, nous avons aussi détaillé les spécificités de la synthèse des stratégies LQR pour amortir les oscillations de la barge indépendamment de l'incidence de la houle.La performance de ces solutions d'amortissement a finalement été évaluée par simulation pour un large éventail de conditions de houle, couvrant les spécifications d'un “ cahier des charges ” que nous présentons. On observe une réduction des oscillations en roulis de la barge qui peut atteindre un facteur 4 par rapport à l'éolienne flottante sans TLCD. Ces résultats nous montrent que le dispositif TLMCD que nous proposons est un dispositif intéressant pour amortir de manière significative, robuste et économiquement abordable notre système. / Thanks to the recent policies of subsidizing renewables energies, constructions of offshore wind farms are booming all over the world. Yet, fixed-bottom wind turbine technology, the only one currently deployed, are too costly for deep waters. This hinders the development of wind power. This is why the scientific community has an interest in floating wind turbines (FWT). The cost of these wind turbines does not depend much on water depth. But since the wind turbine is not fixed into the seabed, the mechanical stress caused by the waves significatively raises.To reduce these detrimental loads, different approaches can be used. The litterature already discarded the control of the wind thrust applied on the rotor to compensate the "fore-aft" oscillations of the tower. We focused on stabilizing floating wind turbine by means of an attached damping system placed inside the float, it is a Tuned Liquid Column Damper (a U-tube containing a liquid, TLCD, also known as anti-roll tank), used in other areas. The damper we propose is an active system where TLCD parameters are continuously modified. Parameters are updated according to a strategy defined thanks to an analysis of the interactions between TLCD and the float (referred to as barge) supporting the wind turbine. We modelled the coupled dynamics of the barge and the TLCD in the vertical plan using a Lagrangian approach. We studied the motions of the damped system for a constant head-loss coefficient in the TLCD. The limits of this approach were detailed thanks to the classic results in double oscillators literature. Then, we focused on an active approach involving a time varying of the head-loss coefficient. We proposed Linear Quadratic Regulator and Model Predictive Control strategies to determine the head-loss coefficient. At a later stage, simulations enabled us to discard the MPC strategy as its complexity/performance ratio is rather bad compared to the LQR strategy in this particular case.A more general study of the system, in three dimensions, showed us that the TLCD is not robust against wave incidence. Therefore, we imagined and modeled new dampers inspired by the TLCD, which can damp the float effectively, regardless of the wave incidence. We named those dampers Tuned Liquid Multiple Column Damper (TLMCD).The dampers we propose are active TLMCD. Their designs are based on their dynamic properties and a cost study. We also detailed the specificities of LQR design to ensure the best possible robustness against wave incidence.The performance of the proposed TLMCD dampers was assessed through numerical simulations for a wide range of sea conditions. We observe that barge roll can be reduced by a factor of four compared to the undamped FWT. These results show us that the TLMCD we propose is interesting to damp significantly, robustly and economically our FWT.

Ce mémoire présente une étude théorique et expérimentale de joints annulaires à bague flottante ainsi que de joints rainurés segmentés, destinés à assurer l’étanchéité dynamique au sein de machines tournantes à haute vitesse dans les domaines aéronautique et aérospatial. Des joints annulaires à bague flottante ont été testés sur un banc d’essais dédié au sein de l’institut Pprime pour de multiples configurations de vitesse de rotation et de différence de pression étanchée. La réponse dynamique des joints par rapport aux vibrations du rotor a été étudiée pour différentes amplitudes de l’excitation. Certains résultats issus de cette étude ont été confrontés à une modélisation numérique basée sur les équations de mouvement d’un joint soumis aux forces d’inertie, aux forces hydrodynamiques dans son étanchéité principale et aux forces de frottement à l’étanchéité secondaire. Le coefficient de frottement à l’étanchéité secondaire a été estimé à partir du modèle de Greenwood et Williamson, appliqué au cas d’un régime de lubrification mixte. Les comparaisons réalisées valident le modèle numérique utilisé, qui reproduit le comportement d’un joint soumis à une excitation rotorique donnée. Un autre modèle est proposé pour le cas des joints rainurés segmentés. Les écoulements au sein des différentes parties d’un tel joint ont été modélisés par des méthodes distinctes. Les forces de frottement sont étudiées par un modèle similaire à celui utilisé dans le cas des bagues flottantes. Une étude paramétrique sur différentes caractéristiques géométriques et de fonctionnement du joint a été menée. / This thesis presents a theoretical and experimental study of floating ring annular seals and radial segmented seals. These seals are designed to prevent leakage inside high-speed rotating machinery used in aeronautics and aerospace applications. Floating ring annular seals were tested on a dedicated test rig inside the Institut Pprime. Various rotation speed and pressure difference configurations were used. The behavior of the floating rings when submitted to rotor vibrations was studied for different excitation amplitudes. Results from this study were confronted to a numerical model based on the equations of motion of the seal. The seal is driven by inertia forces, hydrodynamic forces in the main seal and friction forces on the secondary seal. The friction coefficient on the secondary seal was estimated by Greenwood and Williamson’s model for mixed lubrication. The analysis validates the theoretical model, which reproduces the dynamic behavior of a seal driven by a given rotor excitation. Another model was used to study segmented seals. The flow in each part of such a seal was modeled with various methods. Friction forces were studied with a model similar to that used for floating rings. A parametric study was performed on various geometric and operating parameters.

Les systèmes critiques basés sur l’arithmétique flottante exigent un processus rigoureux de vérification et de validation pour augmenter notre confiance en leur sureté et leur fiabilité. Malheureusement, les techniques existentes fournissent souvent une surestimation d’erreurs d’arrondi. Nous citons Arian 5 et le missile Patriot comme fameux exemples de désastres causés par les erreurs de calculs. Ces dernières années, plusieurs techniques concernant la transformation d’expressions arithmétiques pour améliorer la précision numérique ont été proposées. Dans ce travail, nous allons une étape plus loin en transformant automatiquement non seulement des expressions arithmétiques mais des programmes complets contenant des affectations, des structures de contrôle et des fonctions. Nous définissons un ensemble de règles de transformation permettant la génération, sous certaines conditions et en un temps polynômial, des expressions pluslarges en appliquant des calculs formels limités, au sein de plusieurs itérations d’une boucle. Par la suite, ces larges expressions sont re-parenthésées pour trouver la meilleure expression améliorant ainsi la précision numérique des calculs de programmes. Notre approche se base sur les techniques d’analyse statique par interprétation abstraite pour sur-rapprocher les erreurs d’arrondi dans les programmes et au moment de la transformation des expressions. Cette approche est implémenté dans notre outil et des résultats expérimentaux sur des algorithmes numériques classiques et des programmes venant du monde d’embarqués sont présentés. / Critical software based on floating-point arithmetic requires rigorous verification and validation process to improve our confidence in their reliability and their safety. Unfortunately available techniques for this task often provide overestimates of the round-off errors. We can cite Arian 5, Patriot rocket as well-known examples of disasters. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their numerical accuracy and, in this work, we go one step further by automatically transforming larger pieces of code containing assignments, control structures and functions. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve, by re-parsing, the numerical accuracy of the program results. We use abstract interpretation based static analysis techniques to over-approximate the round-off errors in programs and during the transformation of expressions. A tool has been implemented and experimental results are presented concerning classical numerical algorithms and algorithms for embedded systems.

Depuis une vingtaine d'années, l'industrie de la microélectronique et en particulier le marché des mémoires non-volatiles connaît une évolution considérable, en termes d'augmentation de la capacité d'intégration et de diminution du prix de revient. Ceci a permis au grand public d'accéder aux produits électroniques (téléphones portables, baladeurs MP3, clés USB, appareils photos numériques...) qui connaissent actuellement un énorme succès. Cependant, la miniaturisation des mémoires Flash risque de rencontrer des limitations. C'est pourquoi les industriels et les laboratoires recherchent actuellement de nouvelles voies qui permettraient de prolonger la durée de vie de ces dispositifs. Dans ce contexte, l'objectif premier de cette thèse est l'étude expérimentale et théorique des mémoires non-volatiles à nanocristaux de silicium. Nous avons montré les différentes possibilités d'intégration des nanocristaux de silicium à partir d'un procédé de fabrication standard. Un démonstrateur Flash NOR 32 Mb à nanocristaux de silicium a été réalisé à partir d'un produit ATMEL. Nous nous sommes ensuite intéressés à la caractérisation électrique des cellules et matrices mémoires. Une étude exhaustive de l'influence des conditions de programmation ainsi que des paramètres technologiques sur les performances électriques a été menée. La modélisation de l'effacement Fowler-Nordheim et du « gate disturb » a permis de comprendre l'influence de certains de ces paramètres. Concernant l'écriture par porteurs chauds, nous avons étudié l'influence des conditions d'écriture sur la localisation de la charge à l'aide de simulations TCAD et d'un modèle analytique couplé à des mesures expérimentales.

Il est important que les logiciels pilotant les systèmes critiques (avions, centrales nucléaires, etc.) fonctionnent correctement — alors que la plupart des systèmes informatisés de la vie courante (micro-ordinateur, distributeur de billets, téléphone portable) ont des dysfonctionnements visibles. Il ne s'agit pas là d'un simple problème d'ingéniérie : on sait depuis les travaux de Turing et de Cook que la preuve de propriétés de bon fonctionnement sur les programmes est un problème intrinsèquement difficile.<br /><br />Pour résoudre ce problème , il faut des méthodes à la fois efficaces (coûts en temps et en mémoire modérés), sûres (qui trouvent tous les problèmes possibles) et précises (qui fournissent peu d'avertissements pour des problèmes inexistants). La recherche de ce compromis nécessite des recherches faisant appel à des domaines aussi divers que la logique formelle, l'analyse numérique ou l'algorithmique « classique ».<br /><br />De 2002 à 2007 j'ai participé au développement de l'outil d'analyse statique Astrée. Ceci m'a suggéré quelques développements annexes, à la fois théoriques et pratiques (utilisation de techniques de preuve formelle, analyse de filtres numériques...). Plus récemment, je me suis intéressé à l'analyse modulaire de propriétés numériques et aux applications en analyse de programme de techniques de résolution sous contrainte (programmation semidéfinie, techniques SAT et SAT modulo théorie).