Description
- The OptiTrust framework provides programmers with means of optimizing their programs via source-to-source transformations. The framework currently supports array-manipulating programs written in a subset of C syntax.
- OptiTrust leverages static analyses based on a subset of Separation Logic to justify the that the transformations applied are semantic-preserving.
- OptiTrust supports source-to-source tranformations that preserve separation logic derivations, allowing to validate the property that the final optimized code satisfies the same specification as the unoptimized input program.
A complete description of OptiTrust as of September 2025 may be found in
Guillaume Bertholon's PhD thesis. [PDF]
OptiTrust is work in progress.
OptiTrust is open source, and open to collaboration. Hosted on
[Github].
Don't hesitate to get in touch with Arthur Charguéraud or Thomas Kœhler.
Publications
- OptiTrust: an Interactive Framework for Source-to-Source Transformations
by Arthur Charguéraud, Begatim Bytyqi, Damien Rouhling, and Yann Barsamian.
[HAL]
- OptiTrust: an Interactive Optimization Framework
by Thomas Kœhler, Arthur Charguéraud, Begatim Bytyqi, Damien Rouhling, and Yann Barsamian.
[HAL]
- Interactive Source-to-Source Optimizations Validated using Static Resource Analysis
by Guillaume Bertholon, Arthur Charguéraud, Thomas Kœhler, Begatim Bytyqi, and Damien Rouhling.
[ACM]
- Source-to-Source Optimizations Validated using Separation Logic
by Guillaume Bertholon, Arthur Charguéraud, and Thomas Kœhler
[HAL]
- Bidirectional Translation between a C-like Language and an Imperative Lambda-calculus
by Guillaume Bertholon and Arthur Charguéraud
[HAL]
- OptiTrust: Producing Trustworthy High-Performance Code via Source-to-Source Transformations
by Guillaume Bertholon, Arthur Charguéraud, Thomas Kœhler, Begatim Bytyqi, and Damien Rouhling.
[PDF]
- Interactive compilation via trustworthy source-to-source transformations
PhD thesis of Guillaume Bertholon, advised by Arthur Charguéraud.
[PDF]
Contributors
The OptiTrust project is currently lead by Arthur Charguéraud (Inria and Université de Strasbourg) and
Thomas Kœhler (CNRS and Université de Strasbourg).
The project was initiated in 2019 by Arthur Charguéraud.
Students and postdocs
- Yanni Lefki, PhD student, since 2025, works on extending OptiTrust with support for pattern-matching, and with support for producing assembly code.
- Elian Morel, Master intern from ETHZ, since May 2025, works on applying OptiTrust to optimize a LLM inference code, and contributes to improving elaboration in the typechecker.
- Julien François de Castelnau, Master intern from EPFL, since September 2025, works on applying OptiTrust to produce GPU code.
Other researchers involved in the ANR project
- 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.
- Pauline Bonnet, M2 intern, 3 months in 2025, worked on correctness criteria for the parallelization scheme involved in the particle-in-cell case study.
- Guillaume Bertholon, PhD student March 2022 - August 2025, implemented the typechecker, worked on correctness criteria, and contributed many other improvements to the framework.
Funding
- ANR OptiTrust: from October 2022 to September 2028, the French National Research Agency (ANR) funds a 2-year postdoc position, a 2-year engineer position, internship positions, contributions by 2 CEA researchers, as well as travel and equipment expenses.
- ENS PhD Grant: the PhD of Guillaume Bertholon, from September 2022 to September 2025, was funded by a PhD grant "contrat doctoral spécifique normaliens" (CDSN).
- Inria exploratory action: from September 2019 to August 2022, Inria funded a 11-month postdoc position, a 18-month engineer position, a 2-month internship position, as well as travel and equipment expenses.