Accueil > Recherche > Étudiants/Post-docs
Étudiants/Post-docs
Dernier ajout : 7 mars 2019.
Articles de cette rubrique
-
Xavier Poczekajlo
Optimisations de performances de simulateurs sur machines multi-cœurs
Années: 2013 (IRL Ensimag) Sujet: Optimisations de performances de simulateurs sur machines multi-cœurs Résumé: L’objectif initial de l’IRL était d’utiliser les outils de profiling existants (mutrace par exemple) sur le code d’un simulateur parallèle basé sur SystemC, pour identifier les goulots d’étranglements limitant le passage à l’échelle. Une première constatation était qu’utiliser les outils existants n’était pas immédiat, en particulier les informations fournies par mutrace sont difficilement exploitables sur du code utilisant boost::thread. La contribution du stage est donc un outil permettant (...) -
Julien Henry (Thèse)Analyse de programmes par interprétation abstraite
Thèse soutenue le lundi 13 octobre 2014 Années: 2011, 2012, 2013, 2014 (Ph. D) Co-encadrant: David Monniaux Sujet: Analyse de programmes par interprétation abstraite Résumé: Julien a travaillé sur l’analyse statique par interprétation abstraite, qui est une technique permettant de découvrir des propriétés sur un programme (invariants de boucle, ...). Cette technique calcule des surapproximations des états possibles du programme. Le sujet de Julien était de raffiner cette technique en utilisant des procédures de décisions (SMT-solving), pour calculer des invariants plus précis. > .ChampRes (...) -
Tayeb Bouhadiba
Power and temperature models for SystemC/TLM
Années: 2011, 2012 (Post-doc) Co-encadrant: Florence Maraninchi Sujet: Power and temperature models for SystemC/TLM Résumé: Les systèmes sur puces modernes sont équipés d’un ensemble de dispositifs matériels permettant d’éteindre ou de réduire la consommation des composants. Une politique d’utilisation de ces mécanismes, généralement écrite au moins partiellement en logiciel, doit être développée et validée tôt dans le flot de conception. Pendant ce post-doctorat, nous avons proposé des solutions pour permettre la simulation de ces politiques à un haut niveau d’abstraction, en (...) -
Valentin Bousson
Dévelopement d’application en langage synchrone pour un robot LeGO NXT
Années: 2011 (Stage L3) Co-encadrant: Claire Maiza Sujet: Dévelopement d’application en langage synchrone pour un robot LeGO NXT Résumé: L’objectif du stage est de réaliser un démonstrateur des possibilités du langage Lustre pour générer du code embarqué sur brique Légo NXT. Le système comporte plusieurs types de capteurs (son, lumière, ...) et d’actionneurs (moteurs, écran, ...), et donne un bon exemple d’un système embarqué. On peut programmer le processeur nu (ARM), ou utiliser le langage NXC qui permet de faire tourner des programmes sur une machine virtuelle embarquée dans la brique. > (...) -
Henry-Joseph Audeoud
Comparaison d’approches de parallélisation de SystemC
Années: 2011 (Excellence Internship) Co-encadrant: Claire Maiza Sujet: Comparaison d’approches de parallélisation de SystemC Résumé: Ce stage fait suite au M2R de Samuel Jones et au TER de Mohamed Zaim-Wadghiri : nous disposons maintenant de deux approches complémentaires pour l’exécution parallèle de modèles SystemC, mais de peu d’exemples utilisant ces techniques. Le stage de Henry-Joseph consistait d’une part en une comparaison des approches, et d’autre part à écrire quelques exemples de plate-formes SystemC en utilisant l’une ou l’autre des méthodes. > .ChampRes display:none; (...) -
Si-Mohamed Lamraoui
Techniques de compilation dédiées pour le simulateur SystemC (basé sur LLVM)
Années: 2011 (TER UJF, Stagiaire M1) Co-encadrant: Claire Maiza Sujet: Techniques de compilation dédiées pour le simulateur SystemC (basé sur LLVM) Résumé: SystemC is a C++ library allowing the design of the hardware blocks contained in a System-on-chip at different level of abstraction. As SystemC is a C++ library, the programs may be compiled with a common C++ compiler. But these compilers miss a lot of optimization opportunities specific to SystemC programs. In this paper, we introduce a way to improve simulation performances of SystemC programs using the LLVM compiler (...) -
Julien Henry (M2R)
Static Analysis by Path Focusing
Années: 2010, 2011 (M2R) Co-encadrant: David Monniaux Sujet: Static Analysis by Path Focusing Résumé: La vérification de programme consiste à découvrir statiquement des propriétés sur des programmes, comme l’ensemble des valeurs que peuvent prendre les variables durant l’exécution. L’Interprétation Abstraite est une technique permettant de calculer une approximation de cet ensemble, le véritable ensemble étant impossible à calculer en général. Ce rapport s’inscrit dans la lignée des travaux visant à améliorer la précision de l’analyse par interprétation abstraite, et propose une technique (...) -
Samuel Jones
Optimistic Parallelisation of SystemC
Années: 2010, 2011 (M2R) Co-encadrant: Claire Maiza Sujet: Optimistic Parallelisation of SystemC Résumé: Les systèmes sur puce deviennent de plus en plus élaborés et répandus. Le développement de logiciels embarqués nécessite des outils de prototypage virtuel. SystemC est la norme industrielle dans le domaine de la simulation de systèmes sur puce modernes, mais sa performance devient insuffisante. Nous présentons une tentative de parallélisation de SystemC utilisant plusieurs ordonnanceurs indépendants, chacun responsable d’un sous-ensemble des processus SystemC disponibles. Chaque ordonnanceur (...) -
Marc Pegon
Analyse de programmes par interprétation abstraite
Années: 2011 (IRL Ensimag) Co-encadrant: David Monniaux Sujet: Analyse de programmes par interprétation abstraite Résumé: L’interprétation abstraite est une méthode d’analyse statique utilisée dans plusieurs outils industriels d’analyse de programmes. Dans ce document, nous montrons comment il est possible de réaliser très rapidement un analyseur de programmes C par interprétation abstraite à l’aide d’outils biens choisis les bibliothèques LLVM et Apron. Après un bref rappel sur l’interpré- tation abstraite, nous présentons ces outils, puis nous donnons les détails d’implémentation de notre (...) -
Guillaume Sarrazin
Étude d’un algorithme de fermeture causale sur des courbes d’arrivée ayant des parties affines
Années: 2011 (IRL Ensimag) Co-encadrant: Karine Altisen Sujet: Étude d’un algorithme de fermeture causale sur des courbes d’arrivée ayant des parties affines Résumé: ac2lus est un outil utilisant une paire de courbes définissant le flux minimal et maximal d’événements qui peuvent arriver durant un intervalle de temps. Ces courbes sont appelées courbes d’arrivée. Sans aucun traitement, ces courbes peuvent amener l’outil dans une situation de dead-lock à cause de contraintes implicites exprimées par la courbe. Un algorithme de causalification permet d’expliciter les contraintes implicites. La (...) -
Mohamed Zaim-Wadghiri
Années: 2011 (IRL Ensimag) Co-encadrant: Claire Maiza Résumé: SystemC est un langage de description de matériel (HDL : Hardware Description Language) permettant une modélisation de haut niveau des systèmes sur puce (SoC), que ce soit au niveau matériel ou logiciel. C’est une bibliothèque C++ qui modélise chaque bloc matériel du SoC par une classe appelée module, et décrit son comportement à l’aide de processus. La simulation dans SystemC est gérée par un scheduler qui n’est pas préemptif. La simulation est donc dite coopérative et n’exploite qu’un seul processeur sur la machine. L’objet du travail (...) -
Ranjan Ravi
Improving the SPIN backend of PinaVM
Années: 2010 (Stagiaire L3) Co-encadrant: Kevin Marquet Sujet: Improving the SPIN backend of PinaVM > .ChampRes display:none; .Rubrique font-size: larger; font-weight: bold; dl.NoticeRes > dd.ref_biblio padding-left:0px; margin-left: 25px; display: list-item; .SousRubrique color: #909090; font-style: italic; 2023 Preprints, Working Papers, ... ref_biblioAngel Abusleme, Thomas Adam, Shakeel Ahmad, Rizwan Ahmed, Sebastiano Aiello, et al.. The Design and Technology Development of the JUNO Central Detector. 2023. ⟨hal-04338602⟩ Accès au (...) -
Loïc Crétin
Développement d’un mini analyseur statique de code intégré dans Éclipse
Années: 2008 (IRL Ensimag) Co-encadrant: David Monniaux Sujet: Développement d’un mini analyseur statique de code intégré dans Éclipse > .ChampRes display:none; .Rubrique font-size: larger; font-weight: bold; dl.NoticeRes > dd.ref_biblio padding-left:0px; margin-left: 25px; display: list-item; .SousRubrique color: #909090; font-style: italic; Search Results --> Url version détaillée , Url version formatée Criteria : Author : "Lo" Number of occurrences founded : (...) -
Yanhong Liu
Granularity-based interfacing between RTC and timed automata
Années: 2008, 2009 (Post-doc) Co-encadrant: Karine Altisen Sujet: Granularity-based interfacing between RTC and timed automata > .ChampRes display:none; .Rubrique font-size: larger; font-weight: bold; dl.NoticeRes > dd.ref_biblio padding-left:0px; margin-left: 25px; display: list-item; .SousRubrique color: #909090; font-style: italic; 2018 Journal articles ref_biblioHyun Lillehoj, Yanhong Liu, Sergio Calsamiglia, Mariano E. Fernandez-Miyakawa, Fang Chi, et al.. Phytochemicals as antibiotic alternatives to promote growth and enhance host health. (...) -
Romain Salles
Model-checking de programmes Java
Années: 2009 (IRL Ensimag) Co-encadrant: David Monniaux Sujet: Model-checking de programmes Java Résumé: Ce sujet était au départ inspiré du sujet de Loïc Crétin l’année précédente. Vu les difficultés que posaient l’intégration des briques de base, nous avons décidé de nous passer d’un certain nombre d’entre elles : pas de front-end de compilateur complexe, pas de bibliothèque externe. Cette-fois, nous travaillons avec le byte-code Java, et la seule bibliothèque est ASM, qui permet de lire simplement ce byte-code. L’idée est de générer du code pour le model-checker NuSMV, et de l’utiliser pour prouver (...) -
Nabila Abdessaied
Design of a Java Simulator for Fast Prototyping of System-on-chip
Années: 2009 (M2R) Co-encadrant: Giovanni Funchal Sujet: Design of a Java Simulator for Fast Prototyping of System-on-chip Résumé: Le travail effectué dans le présent document porte sur la conception d’un prototype de simulateur trans- actionnel en évitant les idées préconcues et les clichés de SystemC. On identifie les contraintes imposées sur l’exécution d’un modèle transactionnel par un simulateur. On définit dans une seconde phase une ex- tension du langage Java pour la modélisation transactionnelle. Le mécanisme de threads du langage Java est particulièrement adapté pour cette étude. Ainsi on (...) -
Xavier Jean
Étude des performances dans les systèmes embarqués, entre simulation numérique et solution équationnelle
Années: 2009 (Stagiaire M1) Co-encadrant: Karine Altisen Sujet: Étude des performances dans les systèmes embarqués, entre simulation numérique et solution équationnelle Résumé: Les systèmes embarqués actuels sont de plus en plus complexes, et les cycles de développement sont de plus en plus courts. Dès la phase de conception, on souhaite avoir une estimation des performances du système alors qu’aucun prototype physique n’est réalisé, et que le système est seulement décrit à un haut niveau d’abstraction. Pour répondre à la complexité croissante des systèmes, un cadre d’analyse de systèmes modulaires a (...) -
Mohamed Taoufiq El Aissaoui
Modélisation du temps dans un simulateur pour systèmes sur puces
Années: 2010 (IRL Ensimag) Co-encadrant: Giovanni Funchal Sujet: Modélisation du temps dans un simulateur pour systèmes sur puces Résumé: Le but du stage est d’expérimenter de nouvelles primitives pour la modélisation du temps dans jTLM. Lors du stage de Nabila Abdessaied, nous avions déjà ajouté la notion de tâches avec durée connue, et l’idée était cette fois-ci de donner la possibilité au programmeur d’utiliser des tâches de durée inconnue à l’avance (un exemple typique étant une boucle d’attente active). > .ChampRes display:none; .Rubrique font-size: larger; font-weight: bold; (...) -
Florian Guffon
Étude des possibilités d’utilisation de Aspic dans Ac2lus
Années: 2010 (Excellence Internship) Co-encadrant: Karine Altisen Sujet: Étude des possibilités d’utilisation de Aspic dans Ac2lus > .ChampRes display:none; .Rubrique font-size: larger; font-weight: bold; dl.NoticeRes > dd.ref_biblio padding-left:0px; margin-left: 25px; display: list-item; .SousRubrique color: #909090; font-style: italic; -
Rafael Velasquez
Portability with respect to execution model in system-on-chip simulation
Années: 2010 (TER UJF) Co-encadrant: Giovanni Funchal Sujet: Portability with respect to execution model in system-on-chip simulation Résumé: Ce travail a été effectué sur un prototype de simulateur transactionnel pour les systèmes sur puces, appelé jTLM. Il s’agit d’intégrer certaines fonctionnalités pour pouvoir expérimenter différents modèles d’exécution, et mieux comprendre leur impact sur la manière d’écrire le logiciel embarqué. > .ChampRes display:none; .Rubrique font-size: larger; font-weight: bold; dl.NoticeRes > dd.ref_biblio padding-left:0px; margin-left: 25px; display: (...)
| Se connecter |
Plan du site |
Habillage visuel © styleshout sous Licence Creative Commons Attribution 2.5 License