La notion de changement possède un statut particulier en métaphysique. Nos intuitions et nos perceptions les plus communes nous indiquent que la réalité change. Une personne est parfois assise, parfois debout, elle possède parfois un mal de tête et parfois non. Pourtant, le changement rencontre des difficultés, notamment sur la question traditionnelle de l’identité en lien avec l’indiscernabilité. Comment un objet peut-il rester identique à lui-même, en restant le même objet, alors qu’il gagne ou perd des propriétés ? Outre ce problème, les théories physiques de la relativité décrivent un univers dans lequel tout existe éternellement. Comment une chose pourrait changer si elle a toujours les mêmes caractéristiques ? Autrement dit, comment pourrait-il y avoir du changement si tout possède toujours strictement les mêmes caractéristiques ? Ce travail s’intéresse moins à défendre un modèle théorique qui assume le changement, qu’à montrer les exigences qu’il requiert et les contraintes qu’il implique. Nous présentons les conditions nécessaires pour assumer l’existence d’un changement véritable, dans une version maximaliste, selon laquelle des choses apparaissent et disparaissent de la réalité. Cela implique de rejeter l’existence sempiternelle et l’existence nécessaire de tout ce qu’il y a, mais aussi d’assumer une quantification d’ordre supérieur permettant de quantifier sur ce qu’il n’y a pas.

La synthèse de haut-niveau (HLS) est une méthode pour produire une description de matériel à partir d'une spécification haut-niveau, en général écrite en C. Elle fait ainsi intervenir deux modèles d'exécution différents : en entrée, des programmes séquentiels dirigés par leur flot de contrôle, et en sortie, des circuits parallèles dirigés par leurs flots de données. Des techniques d'ordonnancement dynamique permettent d'exploiter le parallélisme du matériel lors de la transition entre ces deux modèles. Cette thèse est un premier pas dans la conception d'un compilateur HLS à ordonnancement dynamique, formellement vérifié dans l'assistant de preuve Rocq. Notre travail se concentre sur une représentation de circuits permettant ce dynamisme, les circuits flot de données, que nous formalisons à deux niveaux : leur spécification au niveau flots de données, et leur implémentation au niveau matériel. Nous étudions deux vues équivalentes de ces circuits : une représentation graphique naturellement adaptée pour les compilateurs, et un langage inductif facilitant les raisonnements et nous permettant ainsi de prouver des méta-propriétés sémantiques, notamment la préservation sémantique. Nous testons la validité de notre travail par rapport à Dynamatic, un outil HLS à ordonnancement dynamique utilisant ces mêmes circuits.

Les systèmes de prédiction fondés sur l'apprentissage automatique sont désormais largement accessibles mais restent trop souvent opaque, s'apparentant à des boîtes noires pour leurs utilisateurs. L'audit, en tant qu'évaluation indépendante est un outil essentiel à la gouvernance de ces systèmes. Cependant, la facilité de détection des audits et leurs conséquences potentiellement coûteuses pour le fournisseur du système rend les audits en boite noire particulièrement vulnérables aux dissimulations. Cette thèse explore les limites de l'audit en boîte noire et présente trois contributions pour y remédier : la formalisation de l'audit robuste comme un problème de construction d'une _connaissance a priori_ pour l'auditeur, l'étude de l'apport de la connaissance de la classe d'hypothèses par l'auditeur, et enfin l'introduction d'une technique d'empreinte de modèle pour détecter les modifications du système post-audit.

Les systèmes embarqués sont davantages vulnérables aux radiations avec l'utilisation de petits transistors, de faibles tension d'allimentation, etc. Les méthodes standards de tolérance aux fautes telles que la redondance par triplication (TMR) induisent des surcoûts en surface. La plupart des travaux sur l'estimation du pire temps d'exécution (WCET), nécessaire pour la guarantie des temps, ne considèrent pas de fautes ou seulement celles liées aux mémoires, le processeur supposé sans fautes, ce qui est dangereux en cas de fautes. L'ordonnancement avec réplication de tâches entraîne des surcoûts temporels et conduit au surdimensionnement. Pour pallier ces limitations, cette thèse améliore l'analyse de vulnérabilité en considérant les impacts fonctionnels et temporels pour des systèmes sous fautes, démontrant l'impact des fautes sur l'estimation du WCET sur un processeur RISC-V à base de Synthèse de Haut-Niveau (HLS). De plus, cette thèse propose des techniques de locksteps peu complexes et peu coûteuses pour la tolérance, grâce à une détection de fautes très rapide, et des mécanismes de rollback à impact temporelle minime, pour restaurer l'état correct du processeur. Enfin, une analyse de la fiabilité de programmes optimisés en considérant plusieurs entrées et niveaux d'optimisations, est proposée et utilisée pour apporter une réplication sélective d'instructions.

Les dispositifs thermoélectriques peuvent convertir directement l’énergie thermique en électricité. Avec le développement rapide des dispositifs électroniques portables, la capacité d’auto-alimentation et la flexibilité mécanique de ces dispositifs sont devenues essentielles. Les matériaux chalcogénures classiques, tels que Bi₂Te₃ et Sb₂Te₃, présentent d’excellentes performances thermoélectriques près de la température ambiante, mais souffrent d’une faible flexibilité en raison du manque de plans de glissement suffisants pour la relaxation des contraintes lors de la flexion. Afin de relever ces défis, ce travail propose une stratégie de régulation multidimensionnelle. Dans un premier temps, des couches minces de chalcogénures ont été fabriquées par dépôt physique en phase vapeur sur des substrats flexibles. Ensuite, l’hybridation et le dopage ont été employés pour améliorer les propriétés thermoélectriques. Plus précisément, l’incorporation de MAPbI₃ dans Bi₂Te₃ et Sb₂Te₃ induit des diffusions interfaciales et des micro-contraintes, améliorant ainsi la mobilité des porteurs et l’orientation préférentielle. Le dopage à l’aluminium dans Cu₂Se élargit la bande interdite et optimise le facteur de puissance, tandis que le dopage au tellure dans Ag₂Se favorise une croissance orientée et ajuste favorablement le transport de charge. Enfin, une ingénierie de l’axe neutre a été mise en œuvre en positionnant les films thermoélectriques près du plan neutre pour minimiser les contraintes de flexion et réduire la formation de fissures lors de la déformation, améliorant ainsi considérablement la flexibilité et la stabilité cyclique des films et des dispositifs. Des couches minces et des dispositifs thermoélectriques, performants et flexibles, ont été ainsi obtenus.

La maladie de Parkinson est la deuxième maladie neurodégénérative la plus répandue dans le monde. L’apparition des premières modifications physiologiques liées à la maladie peuvent apparaître jusqu’à 15 ans avant les premiers tremblements. L’objectif de ces travaux est de développer des méthodes d’IRM quantitatives permettant de quantifier avec précision deux neuromarqueurs de la maladie. Le premier neuromarqueur identifié est un dépôt anormal de fer dans les noyaux gris centraux du cerveau. Des approches d’acquisition IRM pondérées en susceptibilité magnétique ont été optimisées pour obtenir un temps d’acquisition réduit couplé avec une quantification robuste. La partie reconstruction des cartes de susceptibilité magnétique a permis d’identifier une chaîne de traitement suffisamment robuste pour distinguer deux groupes d’âge. Le second neuromarqueur est l’agrégation la protéine alpha-synucléine. Des approches d’acquisition par CEST (chemical exchange saturation transfer) ont été développées pour cibler au mieux les protéines de manière non-invasive. Une séquence a notamment été développée en ce sens. Ces différentes approches ont permis d’affiner la quantification et visualisation de neuromarqueurs liés à la maladie de Parkinson. Elles pourront servir en clinique à orienter au plus tôt les patients vers une offre thérapeutique adaptée.

Cette thèse explore comment la chimie de surface, la morphologie et les propriétés plasmoniques de nanomatériaux d’or et d’argent influencent leur comportement électrocatalytique, en particulier pour la réduction de l’oxygène. Des nanoparticules de taille, de forme et de fonctionnalisation contrôlées servent de systèmes modèles afin d’évaluer l’impact de leurs propriétés physico-chimiques sur l’activité, la sélectivité et les effets induits par la lumière. Les agents coiffants classiques, CTAB et citrate, décorant les nanomatériaux, sont comparés à des couches moléculaires greffées par diazonium à base de calix[4]arène, permettant d’obtenir des interfaces plus définies. L’irradiation par laser permet d’examiner des effets induits par les propriétés plasmoniques des notamment effets nanomatériaux, photothermiques, génération de porteurs chauds et amplification du champ électromagnétique. En combinant analyses optiques, caractérisations de surface et mesures électrochimiques, ce travail montre comment l’illumination résonante et la nature des ligands modulent les voies réactionnelles et le transfert de charge. L’étude de met en évidence le rôle déterminant de la structure, de l’agrégation et la fonctionnalisation des nanoparticules dans les performances catalytiques, offrant des pistes pour concevoir des catalyseurs photo-actifs optimisés.

L'analyse flots de données est une technique d'analyse statique qui détermine des informations sur la propagation des données lors de l'exécution d'un programme informatique, sans exécuter le programme. Ces informations peuvent être notamment utilisées pour optimiser le programme lors de sa compilation. Réaliser une analyse flots de données consiste en général à résoudre un système d'équations. En dehors des méthodes traditionnelles utilisées pour résoudre de tels systèmes, d'autres techniques ont été développées. L'une d'entre elles, qui a été proposée par Bourdoncle en 1993, consiste à pré-calculer une stratégie de résolution de manière à résoudre ensuite le système plus efficacement. Cette thèse vise à développer des solveurs formellement vérifiés, qui se basent sur cette technique de résolution. Premièrement, nous proposons une formalisation rigoureuse de la notion de tri topologique faible (WTO) qui permet de représenter la stratégie pré-calculée. Ensuite, nous implémentons et vérifions formellement avec l'assistant de preuve Rocq deux variantes de résolution proposées par Bourdoncle, appelées stratégies itérative et récursive, ainsi que l'algorithme le plus utilisé pour calculer un WTO. Notre développement est entièrement intégré au compilateur formellement vérifié CompCert. Enfin, nous évaluons expérimentalement nos implémentations, en les comparant aux solveurs de CompCert et à une implémentation non vérifiée du calcul du WTO.

Ce travail propose un cadre expérimental pour estimer la consommation énergétique des applications cloud-native. Nous montrons que la puissance statique des cœurs, dérivés des courants de fuites, peut atteindre 12% de la consommation d'énergie de l'intégralité de la puce et présentons une méthode en trois étapes pour l'estimer. Notre seconde contribution établit, via une méthode expérimentale, que fréquences Core/Uncore, volume de données et parallélisme dominent la consommation des caches, avec des modèles non linéaires atteignant R2 >= 95%, ouvrant la voie a une extension du capteur RAPL et a des stratégies d'optimisation énergétique.

Le traitement de flux de données (DSP) dans le continuum edge-cloud hétérogène présente des défis majeurs. L'explosion des applications IoT génère des volumes de données sans précédent nécessitant un traitement en quasi-temps réel. Le continuum edge-cloud étend les infrastructures cloud traditionnelles en intégrant des nœuds de calcul de capacités diverses, introduisant une hétérogénéité réseau et de calcul. Les systèmes DSP comme Apache Flink rencontrent des obstacles spécifiques : déséquilibres de flux, variabilité des performances, et complexité du placement d'opérateurs. Nous analysons l'impact de l'hétérogénéité réseau et de calcul sur les performances DSP, et présentons un environnement d'évaluation pour systèmes DSP hétérogènes. Ces contributions visent à améliorer la compréhension des dynamiques complexes et fournir les bases pour exploiter efficacement le traitement géo-distribué.