Années: 2007, 2008, 2009, 2010, 2011 (CIFRE Ph. D) Co-encadrant: Florence Maraninchi Résumé: Consumer electronic devices are made of hardware (the physical part) and software. In the past, the hardware part had to be fabricated first (e.g. prototype boards), then used for developing the software. Transaction-level modeling (TLM) is an attempt to avoid waiting for the hardware to physically exist before starting the development of software. TLM models are abstractions of pieces of (...)
Lire la suite...
Extraction de modèles et vérification formelle de programmes SystemC
Années: 2008, 2009, 2010 (Post-doc) Sujet: Extraction de modèles et vérification formelle de programmes SystemC Résumé: Kevin is involved in the OpenTLM project. This project concerns the modeling/verification of Systems on a Chip (SoC). Kevin’s research area comprises : the modeling of SoC the extraction of formal models the verification of SoC In these areas, Kevin has written different papers and developed a whole verification chain called PinaVM, including all theoretical contributions. This tool is open-source and available here. > .ChampRes display:none; .Rubrique (...)
Lire la suite...
Extraction de contrats 42 à partir de programmes SystemC
Années: 2010 (IRL Ensimag) Co-encadrant: Kevin Marquet Sujet: Extraction de contrats 42 à partir de programmes SystemC Résumé: Une implémentation de l’extraction de contrats (dans le formalisme « 42 ») qui avait été définie théoriquement par Tayeb Bouhadiba a été réalisée, en se basant sur le front-end SystemC PinaVM. L’outil est incomplet, mais entièrement automatique. > .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: (...)
Lire la suite...
Analyse de Programme par SMT Solving
Années: 2010 (IRL Ensimag) Co-encadrant: David Monniaux Sujet: Analyse de Programme par SMT Solving > .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 Journal articles ref_biblioMarie Chevalerias, Guillaume Coiffier, Christelle Darrieutort-Laffite, Sophie Godot, Sebastien Ottaviani, et al.. Association between radiographic and functional outcome in vertebral osteomyelitis SPONDIMMO, a 6-month (...)
Lire la suite...
Connection de la chaine d’outils LusSy au model-checker NuSMV
Années: 2007 (Stagiaire L3) Sujet: Connection de la chaine d’outils LusSy au model-checker NuSMV > .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;
Lire la suite...