Jobs & Internships

Funded PostDoc and Ph.D Proposals:

• 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
• 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
• Statically typed API for Structured Documents

Master 1:

• En partenariat avec l’entreprise Aniah :
  • Compilation de graphes représentant des circuits électroniques en formules de logiques pour la vérification de propriété
  • Parcours de graphe efficace avec une structure union-find
  • Encodage d’entiers en booléens dans des formules de logiques pour la vérification de propriété
• Décroissance numérique : quels écosystèmes logiciels pour l’informatique frugale ?
• Good error messages and documentation for OCaml modules via diffing

Master (1 or 2):

• Conception d’un outil de gestion participatif de stockage cloud

Previous proposals:

• CFG Patterns: A new tool to formally verify optimisations in Vellvm
• Compiler Intermediate Representation for Algebraic Data Types
• Graphical Reasoning, in Coq
• Starting September 2021
  High Performance Code Generation for Abstract Data Types
  Gabriel Radanne and Laure Gonnord
• In partnership with the Aniah startup :
  • Theoretical complexity of graph-analysis for electrical circuit error detection
  • Formulation généralisée de contraintes topologiques de circuits électriques
  • Applying Symbolic Model-Checking Techniques to Circuit Electric Verification
• [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
• [2020-21] Christophe Alias and Keiji Kimura (Waseda U.) – High-Performance Compilation Schemes using Dynamic Analysis
• [2020-21] 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