Funded PostDoc and Ph.D Proposals:
- PostDoc/PhD: First Class Compilers with Partial Evaluation and Analytic Macros
- Improving Diagnosis for a Formal Verification Tool for Electrical Circuits at Transistor Level (CIFRE Ph.D in collaboration with Aniah)
- Modular Analysis for Formal Verification of Integrated Circuits at Transistor Level (CIFRE Ph.D in collaboration with Aniah)
- Contact us if you are interested in doing a Ph.D in the team !
Internship proposals:
(The list is far from complete, don’t hesitate to contact us directly to discuss an internship topic that suits your motivations)
Master 2 Research:
- Modular Analysis for Formal Verification of Integrated Circuits at Transistor Level
- Dynamic Shape Analysis for Sparse Tensor Code (+ PhD funding)
- Program Detection by Deep Learning
- Improving Diagnosis Quality and Performances of a Formal Verification Tool for Electric Circuits at Transistor Level
- Dedicated Solver for Formal Verification of Electric Circuits with Multiple Power Supplies
- CFG Patterns: A new tool to formally verify optimisations in Vellvm
- Semantics and Implementation of Actors in Multicore OCaml
- Open Automata meet Session Types
- Optimized Memory Representation for Algebraic Data Types
- Compilation of a DSL based on transducers to SIMD optimized programs
- Confluence in active objects
Master 1:
- En partenariat avec l’entreprise Aniah :
- Décroissance numérique : quels écosystèmes logiciels pour l’informatique frugale ?
- Good error messages and documentation for OCaml modules via diffing
- Compiler Intermediate Representation for Algebraic Data Types
- Graphical Reasoning, in Coq
Previous proposals:
- Starting September 2021
High Performance Code Generation for Abstract Data Types
Gabriel Radanne and Laure Gonnord - In partnership with the Aniah startup :
- [2020-21] Matthieu Moy and Frédéric Suter – Workflow vs. Dataflow : Concepts, défis et simulation pour le calcul haute performance
- Dataflow explicit futures: Formalisation and/or experimentation
- Simulation et outils de debug pour réseaux de processus
- [update 2020-21] POM (Lyon 1) with LG : frontend pour des analyses statiques, et outils pour l’édition numérique
- As part of the POLYTRACE Inria exploratory action, Christophe Alias with Keiji Kimura (Japan) – High-Performance Compilation Schemes using Dynamic Analysis
- As part of the HLSIMU projet Emergence ENS, Christophe Alias, with Matthieu Moy – Stratégies de compilation pour la synthèse de circuits
- [2021-2022] Gabriel Radanne and Laure Gonnord – Type indexing in OCaml: search and find functions in a large ecosystem
- [update 2020-21]: Yannick Zakowski with Ludovic Henrio – A parameterized bisimulation for interaction trees
- [update 2020-21]: Ludovic Henrio with Rabéan Ameur Boulifa and Eric Madelaine – Refinement for open automata
- [update 2020-21]: As part of the CAPESA Project, LG/MM/LH with Sebastien Mosser (Montreal) rewritingCode and Study Docker with compilation techniques
- [update 2020-21] LG with C. Collange (Inria Rennes): Static analysis for GPUs
- [update 2020-21] LG/YZ : Static Analysis in the certified SSA-compiler VELLVM.
- [update 2020-21]: As part of the CODAS Project LG with C. Fuhs (London) Scheduling data-structures with term rewriting techniques.
- Dataflow explicit futures: Formalisation and/or experimentation
- Dynamic Allocation in Embedded Systems with Several Memory Types (in collaboration with CITI lab)
- Code Generation for Simulation of Parallel Process Networks
- Scalability of the interference analysis for a multi-core platform
- Interference analysis for the new Kalray MPPA3 many-core
- Programming models for optimised compilation (pdf)
- Hardware Compilation: Recover the FIFOs!
- Ordonnancement de processus sous contrainte de pipeline
- Hierarchical Parallelization (version française :Parallélisation Hiérarchique)
- Analyse de WCET pour réseaux de processus