Direction scientifique
Transfert de connaissances vers l'industrie

Nos Thèses par thème

Algorithmes prouvés de simplification et de résolution pour la preuve de programmes

Département Ingénierie Logiciels et Systèmes (LIST)

Laboratoire pour la Sûreté du Logiciel

Master en méthodes formelles

01-09-2020

SL-DRT-20-0396

loic.correnson@cea.fr

La plateforme Frama-C développée au CEA permet la vérification formelle de programmes critiques. Elle est utilisée de manière industrielle dans différents domaines, comme l'aéronautique ou l'énergie, pour garantir l'absence de défaut de programmes C quelque soient leur conditions d'utilisation. Une garantie d'absence de bug ne peut être obtenue qu'en utilisant des outils de raisonnement automatique, que ce soit des assistants de preuve (Coq, PVS, HOL) ou des solveurs SMT (Z3, CVC4, Alt-Ergo). Pour le passage à l'échelle de ces techniques sur des codes industriels, il est cependant nécessaire de passer par une étape de simplification préalable des objectifs de preuve. Au sein de Frama-C, nous avons pour cela développé le moteur Qed qui est chargé de cette étape critique de simplification. Cela a permis notamment des gains d'automatisation considérables dans l'automatisation des preuves de programmes développés par Airbus, conduisant à la généralisation de cette approche dans leur processus de production industrielle. Depuis ses premiers développements en 2015 le moteur Qed a connu de nombreux perfectionnements qui sont de plus en plus difficiles à developper tout en s'assurant de la correction des simplifications réalisées. Il devient maintenant nécessaire d'automatiser la vérification du moteur Qed lui-même. Le but de la thèse est de re-developper entièrement Qed dans l'environnement de preuve Why-3 en spécifiant et en vérifiant la correction de ses algorithmes de simplification. A terme, le code extrait du développement Why-3 serait utilisé en remplacement complet du moteur actuel au sein de Frama-C.

Télécharger l'offre (.zip)

Techniques de sécurisation matérielle d'algorithmes de cryptographie tirant partie du calcul en mémoire

Département Architectures Conception et Logiciels Embarqués (LIST-LETI)

Laboratoire Intégration Silicium des Architectures Numériques

Master 2 microelectronique

01-10-2020

SL-DRT-20-0401

simone.bacles-min@cea.fr

Le laboratoire LISAN (Laboratoire Intégration Silicium et Architecture Numérique) développe et conçoit des systèmes sur puces (SoC) innovants à base d'architectures multic?urs ainsi que des architectures basse consommation dédiées à l'Internet des Objets (Internet of Things - IoT). Le domaine de l'IoT remet à plat de nombreux prérequis, notamment au niveau de la sécurité des objets connectés autonomes en énergie. Les nouvelles architectures se veulent les plus économes en énergie possible. L'implémentation de la sécurité dans l'IoT doit donc elle aussi être guidée par l'énergie disponible, sans pour autant mener à des failles de sécurité. Une mémoire intelligente, appelée C-SRAM, permettant de faire des calculs au sein de la mémoire a été conçue au sein du laboratoire. L'objectif de la thèse est d'étudier les possibilités de cette mémoire du point de vue de la sécurité. Les propriétés intrinsèques de cette mémoire intelligente permettent d'envisager l'implémentation de plusieurs algorithmes et surtout de nouvelles contre-mesures contre les attaques physiques combinées (canaux auxiliaires et en fautes.

Télécharger l'offre (.zip)

Intégration de réseaux de neurones à base d'oscillateurs verrouillés par injection

Département Architectures Conception et Logiciels Embarqués (LIST-LETI)

Laboratoire Intégration Gestion d'Energie Capteurs et Actionneurs

Ecole Ingénieur Electronique

01-09-2020

SL-DRT-20-0418

franck.badets@cea.fr

Nouveaux paradigmes de calculs, circuits et technologies, dont le quantique (.pdf)

Les réseaux de neurones ont fait la preuve de leur supériorité par rapport aux architectures de calcul de type Von Neumann pour les opérations de classification complexes. L'embarquement de réseaux de neurones proche du capteur (Edge IA) est souhaitable car elle permettrait de réduire la consommation d'énergie des réseaux de capteur sans fil en donnant plus d'autonomie de décision aux capteurs et en limitant le nombre de communication nécessaires entre les capteurs et le centre de ressource en calcul. Il existe actuellement un axe de recherche visant à diminuer sensiblement la consommation des neurones afin de répondre aux besoins de l'Edge IA. A côté des implémentations purement numériques, des solutions analogiques voient le jour. Le but de la thèse est de démontrer la faisabilité de l'intégration sur silicium d'un réseau de neurones Ultra Faible Consommation utilisant des Oscillateurs Verrouillés par Injection (ILO) comme neurone. Le candidat à cette thèse doit avoir une bonne connaissance des domaines de l'apprentissage statistique et des réseaux de neurone en particulier. Il doit également avoir un bon niveau en électronique analogique. L'approche théorique nécessitera de bonnes aptitudes mathématiques et une bonne connaissance des langages de modélisation tel que python. Le travail de thèse doit aboutir à l'intégration d'un réseau de neurones à ILOS sur silicium ainsi qu'à la démonstration de sa capacité d'apprentissage, pour une consommation à l'état de l'art.

Télécharger l'offre (.zip)

Nanocomposites avancés pour l'impression additive

Département des Technologies des NanoMatériaux (LITEN)

Laboratoire Synthèse et Intégration des Nanomatériaux

Ingénieur / Master 2 en chimie - matériaux

01-10-2020

SL-DRT-20-0419

thomas.pietri@cea.fr

Fabrication additive, nouvelles voies d'économie de matériaux (.pdf)

Les objectifs scientifiques proposés sont à la croisée des nanomatériaux et des techniques d'impression additive. Différentes technologies d'impression 3D de matrices polymériques ont été développées, permettant la conversion d'un modèle numérique en modèle physique avec une grande précision. Mais, sans doute en raison du développement très récent de ces technologies, les matériaux actuellement disponibles présentent des limitations pour de nombreuses applications, qui pourraient être résolues par l'utilisation de nanocomposites à haute performance. Le travail qui sera réalisé dans cette thèse consistera à réaliser la synthèse et la fonctionnalisation de nanomatériaux à forts facteurs de formes (nanofils, nanotubes), puis à les intégrer dans des matrices polymères. Après caractérisation des propriétés des nanocomposites ainsi obtenus, des fils de nanocomposites seront réalisés pour être utilisés dans la fabrication d'objets par impression 3D. Les nanocomposites à haute performance visés seront utilisés pour la réalisation de pièces ayant une forte conduction électrique et/ou thermiques. Des applications pour le domaine de la santé seront aussi envisagées.

Télécharger l'offre (.zip)

Etude des mécanismes de dégradation et Fiabilité dynamique des composants GaN sur Si

Département Composants Silicium (LETI)

Laboratoire de Caractérisation et Test Electrique

MASTER2 ou Ecole d'Ingenieur sciences des matériaux, électronique

01-10-2020

SL-DRT-20-0430

william.vandendaele@cea.fr

Matériaux et procédés émergents pour les nanotechnologies et la microélectronique (.pdf)

Les composants de puissance GaN sur Si sont aujourd'hui vus comme la prochaine génération de composants « mass market » pour la conversion d'énergie électrique à haut rendement. Dans ce cadre, le LETI développe sa propre filière GaN sur Si (compatible CMOS) allant du substrat au module final. Ces dispositifs doivent opérer des commutations entre un état de forte tension (~650V) et de fort courant (~20A) à des fréquences élevées (> 100kHz). Les performances statiques et dynamiques étant établies, il est nécessaire de tester la fiabilité de ces composants lors des état de fort stress (OFF et commutation OFF -> ON) ainsi que de comprendre les mécanismes de dégradation sous-jacent afin de stabiliser la technologie et de prétendre à un transfert industriel. Dans la continuité du stage sur le développement des mesures dynamiques sur dispositifs GaN sur Si, le candidat aura en charge : - La finalisation des solutions de mesures ainsi que leurs évolutions notamment pour porter ces tests de dégradation sur prober (détermination de la faisabilité et des limitations) - De l'étude approfondie de la dégradation des performances électriques des transistors (Ron, Vth, Sw?) ou des diodes (Vf, Ron) lors de stress de type AC ou DC afin de déterminer les mécanismes susceptibles de diminuer la fiabilité des composants - La réalisation et la détermination des limites de fonctionnement de la technologie GaN sur Si via des tests de type SSOA (Switching Safe Operating Area) - La compréhension et la localisation des points de défaillance sur les transistors et la diodes GaN sur Si - De proposer des solutions techniques afin d'augmenter la durée de vie des composants auprès du laboratoire LC2E Le candidat devra faire preuve d'esprit d'équipe, de curiosité et d'une grande autonomie

Télécharger l'offre (.zip)

Optimisation de l'interface diélectrique/GaN pour la grille MIS des transistors de puissance

Département Composants Silicium (LETI)

Laboratoire Composants Electroniques pour l'Energie

Master Microélectronique ou Science des Matériaux

01-09-2020

SL-DRT-20-0432

laura.vauche@cea.fr

Matériaux et procédés émergents pour les nanotechnologies et la microélectronique (.pdf)

Sur le marché de l'électronique de puissance, un des challenges principaux pour le déploiement des technologies à base de GaN est le développement de composants normally-OFF fiables. Dans le cas de transistors GaN avec une grille MIS, les propriétés de l'interface diélectrique/GaN sont cruciales. L'objectif de cette thèse est d'optimiser l'interface diélectrique/GaN pour la grille MIS des transistors de puissance. Pour cela : 1. La qualité de l'interface diélectrique/GaN sera contrôlée par XPS (X-ray Photoelectron Spectroscopy). Cette technique permet d'étudier le degré d'oxydation de la surface du GaN. Des analyses complémentaires par ToF-SIMS (Time of Flight Secondary Ion Mass Spectrometry) et HRTEM (High Resolution Transmission Electron Microscopy) seront effectuées pour obtenir des informations concernant la composition chimique et la structure cristalline des matériaux. 2. La qualité des composants à base de GaN sera en parallèle étudiée grâce à la caractérisation des propriétés électriques de capacitances et transistors (mobilité, résistance à l'état passant et sous le canal, tension de seuil, hystérésis), ainsi que des mesures électriques fines (extraction états d'interface Dit, fiabilité) 3. La corrélation des résultats matériaux et électriques permettra de déterminer, de manière comparative, si l'interface oxyde/GaN est de bonne qualité afin de choisir les procédés de fabrication les plus adaptés. Pour ce faire, l'impact des différentes étapes de fabrication (nettoyage chimique, gravure, stripping, traitements plasma et recuits) sera évalué.

Télécharger l'offre (.zip)

115 (Page 3 sur 20)
first   previous  1 - 2 - 3 - 4 - 5  next   last
-->

Voir toutes nos offres