Accueil > Recherche > Stages/emplois
Stages/emplois
Dernier ajout : 10 juin 2024.
Cette section contient des offres de stages, emplois et thèses dans lesquels je suis impliqué.
Articles de cette rubrique
-
Improving Diagnosis for a Formal Verification Tool for Electrical Circuits at Transistor Level
CIFRE Ph. D with the Aniah Compagny
-
Modular Analysis for Formal Verification of Integrated Circuits at Transistor Level
CIFRE Ph. D with the Aniah Compagny
-
[TAKEN] Dedicated Solver for Formal Verification of Electric Circuits with Multiple Power Supplies
-
Improving Diagnosis Quality and Performances of a Formal Verification Tool for Electric Circuits at Transistor Level
-
[Taken] Applying Symbolic Model-Checking Techniques to Circuit Electric Verification
Aniah is a Start-up that offers tools for analyzing semiconductor manufacture circuits. Aniah has introduced algorithms that significantly pushes the boundaries of the size of analyzable circuits, from a few hundred thousand elements to several trillion. Aniah is starting a collaboration with the Laboratoire de l’Informatique du Parallélisme (LIP) and the Verimag laboratory to consolidate and generalize its approach by supplementing its practical results with a theoretical backbone. One of the objectives of this study is to explore the applicability of state-of-the-art model-checking (...) -
[Taken] Theoretical complexity of graph-analysis for electrical circuit error detection
Collaboration between LIP and the Aniah Startup.
Aniah is a Start-up that offers tools for analyzing semiconductor manufacture circuits. Aniah has introduced algorithms relying on hierarchical graph decompositions that significantly pushes the boundaries of the size of analyzable circuits, from a few hundred thousand elements to several trillion. Aniah is collaborating with the Laboratoire de l’Informatique du Parallélisme (LIP) to consolidate and generalize its approach by supplementing its practical results with a theoretical backbone. The overall goal of the internship is to study the theoretical complexity of existing algorithms, (...) -
[Pris] Un Enigma moderne
Sujet déjà réservé pour Tom Montauriol. Boîte de chiffrement / déchiffrement sur raspberry pi. Le principe : on insère une clé USB avec les documents à chiffrer / déchiffrer dessus et après on fournit la clé de chiffrement. Si la clé USB n’est pas chiffrée quand on l’insère, elle l’est quand on la retire. Si la clé USB est chiffrée quand on l’insère, elle ne l’est plus quand on la retire. Pour fournir la clé de chiffrement plusieurs solutions : - Une autre clé USB avec la clé dessus (ou plusieurs USB avec des fragments de la même clé, ou juste plusieurs clés) - On scanne un QR code qui représente la (...) -
[CANCELED] [M2 Research] Code Generation for Simulation of Parallel Process Networks
-
[CANCELED][Thèse] Vérification formelle de réseaux de processus comme représentation intermédiaire d’un compilateur
https://jobs.inria.fr/public/classic/fr/offres/2018-00436 -
[PRIS] Programmation parallèle pour la modélisation des systèmes embarqués
Ce sujet est déjà pris et n'est conservé que pour référence Laboratoire : Verimag Équipe : Équipe SYNCHRONE Encadrant : Matthieu.Moy@imag.fr Thème général SystemC est une bibliothèque pour C++ qui permet de modéliser des systèmes matériels complexes. C'est devenu un outil incontournable dans la conception des systèmes sur puces (contenus dans des téléphones portables, télévision numériques, ...). Le parallélisme du système modélisé est exprimé avec des processus SystemC, qui s'exécutent séquentiellement pendant la simulation (on parle de simulation « coopérative »). La simulation coopérative (...) -
[PRIS] Simulation distribuée pour les systèmes embarqués
Ce sujet est déjà pris et n'est conservé que pour référence Laboratoire : Verimag Équipe : Équipe SYNCHRONE Encadrant : Matthieu.Moy@imag.fr Thème général SystemC est une bibliothèque pour C++ qui permet de modéliser des systèmes matériels complexes. C'est devenu un outil incontournable dans la conception des systèmes sur puces (contenus dans des téléphones portables, télévision numériques, ...). Le parallélisme du système modélisé est exprimé avec des processus SystemC, qui s'exécutent séquentiellement pendant la simulation (on parle de simulation « coopérative »). La simulation coopérative (...) -
[TAKEN] Visualisation graphique de traces de simulation de systèmes sur puces
Ce sujet est déjà pris et n'est gardé que pour mémoire Encadrant : Matthieu Moy Matthieu.Moy@imag.fr Thème général Les systèmes embarqués modernes (smartphones, box de fournisseurs d’accès internet, ...) sont réalisés avec un mélange de logiciel et de matériel, développés l’un pour l’autre. Étant donné la complexité de ces systèmes, il n’est plus possible aujourd’hui d’attendre la disponibilité du matériel pour développer le logiciel, et il est donc nécessaire d’utiliser des simulateurs. Le laboratoire Verimag travaille depuis une dizaine d’années avec STMicroelectronics sur le simulateur SystemC (basé sur (...) -
[PRIS] Optimisations de performances de simulateurs sur machines multi-cœurs
Sommaire Contexte Scientifique Compétences attendues Contexte de travail Sujet proposé Ce sujet est déjà pris et n'est conservé que pour référence Laboratoire : Verimag (http://www-verimag.imag.fr/) Équipe : SYNCHRONE (http://www-verimag.imag.fr/SYNCHRONE) Encadrants : Matthieu Moy <Matthieu.Moy@imag.fr> Contexte Scientifique Les systèmes embarqués modernes (smartphones, box de fournisseurs d’accès internet, …) sont réalisés avec un mélange de logiciel et de matériel, développés l’un pour l’autre. Étant donné la complexité de ces systèmes, il n’est plus possible aujourd’hui (...) -
[TAKEN] Techniques de compilation dédiées pour un langage spécifique à un domaine (SystemC)
Sommaire Scientific Context Subject Required Skills Work context Laboratory : Verimag (http://www-verimag.imag.fr/) Team : SYNCHRONE (http://www-verimag.imag.fr/SYNCHRONE) Supervisor : Matthieu Moy <Matthieu.Moy@imag.fr> Scientific Context The silicon industry is widely adopting a methodology called Transaction-Level Modeling (TLM), that consists essentially in writing abstract, but yet executable models the hardware contained in a Chip. SystemC is a C++ library used for the description of SoCs at different levels of abstraction, including TLM. It comes with a (...) -
[PRIS] Simulation coopérative et parallèle : expérimentations sur le scheduler SystemC
Proposition de stage de Master Recherche
Ce sujet est déjà pris, et gardé ici seulement pour archive. laboratoire : Verimag equipe : Équipe SYNCHRONE encadrants : Matthieu.Moy@imag.fr, Claire.Maiza@imag.fr Thème général SystemC est une bibliothèque pour C++ qui permet de modéliser des systèmes matériels complexes (typiquement, les systèmes sur puces contenus dans des téléphones portables, télévision numériques, ...). Le parallélisme du système modélisé est exprimé avec des processus SystemC, qui s'exécutent séquentiellement pendant la simulation (on parle de simulation « coopérative »). La simulation coopérative apporte un certain (...) -
[PRIS] Techniques de compilation dédiées pour le simulateur SystemC (basé sur LLVM)
Sujet de stage M1 ou M2
Ce sujet est déjà pris, et gardé ici seulement pour archive. Laboratory : Verimag (http://www-verimag.imag.fr/) Team : SYNCHRONE (http://www-verimag.imag.fr/SYNCHRONE) Supervisor : Matthieu Moy <Matthieu.Moy@imag.fr> Scientific Context The silicon industry is widely adopting a methodology called Transaction-Level Modeling (TLM), that consists essentially in writting abstract, but yet executable models the hardware contained in a Chip. SystemC is a C++ library used for the description of SoCs at different levels of abstraction, including TLM. It comes with a simulation (...) -
[PRIS] Simulation coopérative et parallèle : expérimentations avec le scheduler SystemC
Proposition de stage TER
Ce sujet est déjà pris, et gardé ici seulement pour archive. laboratoire : Verimag equipe : Équipe SYNCHRONE encadrants : Matthieu.Moy@imag.fr, Claire.Maiza@imag.fr Thème général SystemC est une bibliothèque pour C++ qui permet de modéliser des systèmes matériels complexes (typiquement, les systèmes sur puces contenus dans des téléphones portables, télévision numériques, ...). Le parallélisme du système modélisé est exprimé avec des processus SystemC, qui s'exécutent séquentiellement pendant la simulation (on parle de simulation « coopérative »). La simulation coopérative apporte un certain (...) -
[TAKEN] Implementation and experimentation of dataflow explicit futures
-
Parallélisation automatique d’operations sur matrices creuses
-
[Master 2 Recherche] Ordonnancement de processus sous contrainte de pipeline
Résumé Les opérateurs arithmétiques à virgule flottante utilisés dans les accélérateurs matériels sont pipelinés pour ne pas limiter la fréquence du circuit. Une opération i produit son résultat à la date i+k, avec k le nombre d’étages du pipeline. Si le résultat de i est utilisé par une opération j, j devra attendre que le résultat soit disponible : j>i+k (contrainte de pipeline). Dans le cas contraire, le pipeline de j sera bloqué jusqu’à ce que la donnée soit disponible. L’ordonnancement sous contrainte de pipeline consiste à réorganiser les opérations pour réduire le temps total d’exécution tout en (...)
- 1
- 2
| Se connecter |
Plan du site |
Habillage visuel © styleshout sous Licence Creative Commons Attribution 2.5 License