Funded PostDoc and Ph.D Proposals:<\/h2>\n

\n
• Contact us if you are interested in doing a Ph.D in the team !<\/li>\n<\/ul>\n

  Internship proposals:<\/h2>\n

  (The list is far from complete, don’t hesitate to contact us directly to discuss an internship topic that suits your motivations)<\/p>\n

  Master 2 Research:<\/strong><\/p>\n

  \n
  • Modular Analysis for Formal Verification of Integrated Circuits at Transistor Level<\/a><\/li>\n
  • Dynamic Shape Analysis for Sparse Tensor Code (+ PhD funding)<\/a><\/li>\n
  • Program Detection by Deep Learning<\/a><\/li>\n
  • Improving Diagnosis Quality and Performances of a Formal Verification Tool for Electric Circuits at Transistor Level<\/a><\/li>\n
  • Dedicated Solver for Formal Verification of Electric Circuits with Multiple Power Supplies<\/a><\/li>\n
  • Semantics and Implementation of Actors in Multicore OCaml<\/a><\/li>\n
  • Open Automata meet Session Types<\/a><\/li>\n
  • Optimized Memory Representation for Algebraic Data Types<\/a><\/li>\n
  • Compilation of a DSL based on transducers to SIMD optimized programs<\/a><\/li>\n
  • Confluence in active objects<\/a><\/li>\n
  • Statically typed API for Structured Documents<\/a><\/li>\n<\/ul>\n

    Master 1:<\/strong><\/p>\n

    \n
    • En partenariat avec l’entreprise Aniah :\n
      \n
      • Compilation de graphes repr\u00e9sentant des circuits \u00e9lectroniques en formules de logiques pour la v\u00e9rification de propri\u00e9t\u00e9<\/a><\/li>\n
      • Parcours de graphe efficace avec une structure union-find<\/a><\/li>\n
      • Encodage d’entiers en bool\u00e9ens dans des formules de logiques pour la v\u00e9rification de propri\u00e9t\u00e9<\/a><\/li>\n<\/ul>\n<\/li>\n
      • D\u00e9croissance num\u00e9rique : quels \u00e9cosyst\u00e8mes logiciels pour l’informatique frugale ?<\/a><\/li>\n
      • Good error messages and documentation for OCaml modules via diffing<\/a><\/li>\n<\/ul>\n

        Master (1 or 2):<\/strong><\/p>\n

        \n
        • Conception d\u2019un outil de gestion participatif de stockage cloud<\/a><\/li>\n<\/ul>\n

          Previous proposals:<\/h2>\n

          \n
          • CFG Patterns: A new tool to formally verify optimisations in Vellvm<\/a><\/li>\n
          • Compiler Intermediate Representation for Algebraic Data Types<\/a><\/li>\n
          • Graphical Reasoning, in Coq<\/a><\/li>\n
          • <\/li>\n
          • Starting September 2021
            \nHigh Performance Code Generation for Abstract Data Types <\/a>
            \nGabriel Radanne and Laure Gonnord<\/li>\n
          • In partnership with the Aniah<\/a> startup :\n
            \n
            • Theoretical complexity of graph-analysis for electrical circuit error detection<\/a><\/li>\n
            • Formulation g\u00e9n\u00e9ralis\u00e9e de contraintes topologiques de circuits \u00e9lectriques<\/a><\/li>\n
            • Applying Symbolic Model-Checking Techniques to Circuit Electric Verification<\/a><\/li>\n<\/ul>\n<\/li>\n
            • [2020-21] Matthieu Moy and Fr\u00e9d\u00e9ric Suter – Workflow vs. Dataflow : Concepts, d\u00e9fis et simulation pour le calcul haute performance<\/a><\/li>\n
            • Dataflow explicit futures: Formalisation and\/or experimentation<\/a><\/li>\n
            • Simulation et outils de debug pour r\u00e9seaux de processus<\/a><\/li>\n
            • [update 2020-21] POM (Lyon 1) with LG : frontend pour des analyses statiques<\/a>, et outils pour l’\u00e9dition num\u00e9rique<\/a><\/li>\n
            • [2020-21] Christophe Alias and Keiji Kimura (Waseda U.) – High-Performance Compilation Schemes using Dynamic Analysis<\/a><\/li>\n
            • [2020-21] Christophe Alias, with Matthieu Moy – Strat\u00e9gies de compilation pour la synth\u00e8se de circuits<\/a><\/li>\n
            • [2021-2022] Gabriel Radanne and Laure Gonnord – Type indexing in OCaml: search and find functions in a large ecosystem<\/a><\/li>\n
            • [update 2020-21]: Yannick Zakowski with Ludovic Henrio – A parameterized bisimulation for interaction trees<\/a><\/li>\n
            • [update 2020-21]:\u00a0 Ludovic Henrio with Rab\u00e9an Ameur Boulifa and Eric Madelaine – Refinement for open automata<\/a><\/li>\n
            • [update 2020-21]:\u00a0 As part of the CAPESA Project, LG\/MM\/LH with Sebastien Mosser (Montreal) rewritingCode<\/a> and Study Docker with compilation techniques<\/a><\/li>\n
            • [update 2020-21] LG with C. Collange (Inria Rennes): Static analysis for GPUs<\/a><\/li>\n
            • [update 2020-21] LG\/YZ : Static Analysis in the certified SSA-compiler VELLVM<\/a>.<\/li>\n
            • [update 2020-21]: As part of the CODAS Project LG with C. Fuhs (London) Scheduling data-structures with term rewriting techniques<\/a>.<\/li>\n
            • Dataflow explicit futures: Formalisation and\/or experimentation<\/a><\/li>\n
            • Dynamic Allocation in Embedded Systems with Several Memory Types<\/a> (in collaboration with CITI lab)<\/li>\n
            • Code Generation for Simulation of Parallel Process Networks<\/a><\/li>\n
            • Scalability of the interference analysis for a multi-core platform<\/a><\/li>\n
            • Interference analysis for the new Kalray MPPA3 many-core<\/a><\/li>\n
            • Programming models for optimised compilation (pdf<\/a>)<\/li>\n
            • Hardware Compilation: Recover the FIFOs!<\/a><\/li>\n
            • Ordonnancement de processus sous contrainte de pipeline<\/a><\/li>\n
            • Hierarchical Parallelization<\/a> (version fran\u00e7aise :Parall\u00e9lisation Hi\u00e9rarchique<\/a>)<\/li>\n
            • Analyse de WCET pour r\u00e9seaux de processus<\/a><\/li>\n<\/ul>\n

              <\/p>\n","protected":false},"excerpt":{"rendered":"

              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 … Continue reading “Jobs & Internships”<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-70","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/pages\/70","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=70"}],"version-history":[{"count":72,"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/pages\/70\/revisions"}],"predecessor-version":[{"id":749,"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/pages\/70\/revisions\/749"}],"wp:attachment":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=70"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}