Contributors
The OptiTrust project is lead by Arthur Charguéraud (Inria and Université de Strasbourg), who is interested in program verification, program optimization, and mechanized semantics of programming languages.
Students and postdocs
- Guillaume Bertholon, PhD student since March 2022, works on maintaining Separation Logic derivations through transformations, and works on the OCaml front-end.
- Thomas Koehler, postdoc since January 2023 (CNRS researcher starting in Sept. 2024), works on adding static correctness checks for transformations, and develops image processing case studies.
Researchers
- Jens Gustedt (Inria and Université de Strasbourg) served for 10 years on the C standardization committee, in particular as co-editor of the C17 standard.
- Alain Ketterlin (Université de Strasbourg) is an expert in polyhedral transformations, a large class of optimizations for performance-critical loop nests.
- Yannick Zakowski (Inria and ENS Lyon) works on mechanized semantics for programming languages, program logics, and compiler correctness proofs.
- François Pottier (Inria) works on semantics and program logics for OCaml and multicore OCaml, and on mechanized proofs of time and space bounds.
- Xavier Leroy (Collège de France and Inria) is the main architect of the OCaml programming language and of the CompCert formally verified compiler.
- Loïc Correnson (CEA) leads the development of the Frama-C platform for the analysis of C programs.
- Allan Blanchard (CEA) is a researcher involved in the development of Frama-C, in particular the EVA and WP plugins.
- Philippe Helluy (Université de Strasbourg and Inria) works on mathematical and numerical analysis of physical systems, and high-performance implementations of simulations.
- Victor Michel-Dansac (Inria and Université de Strasbourg) is a researcher in applied mathematics, also working on numerical analysis and high-performance simulations.
Past contributors
- Ramon Fernandez Mir, M1 intern, 4 months in 2018, studied the formalization in Coq of data layout transformations.
- Damien Roulhing, postdoc, 11 months in 2019, implemented the core of the OptiTrust framework.
- Begatim Bytyqi, postdoc, 18 months in 2021-2022, extended the transformation library and completed the particle-in-cell case study.
- Anton Danilkin, L2 intern, 2 months in 2021, worked on the import of Rust code into OptiTrust.
- Nicolas Nardino, M2 intern advised by Yannick Zakowski, March-July 2023, worked on a mechanized proof relating the semantics of OptiTrust with that of the CompCert verified compiler.