OptiTrust

Deriving high-performance code via programmer-guided, source-to-source transformations.

Description

  • The OptiTrust framework provides programmers with means of optimizing their C programs via source-to-source transformations, with plans to support a subset of C++ and OCaml.
  • OptiTrust leverages static analyses based on a subset of Separation Logic to justify the correctness of transformations.
  • OptiTrust will soon support trustworthy optimizations of programs that have been fully verified through interactive proofs in Separation Logic.

OptiTrust is work in progress.
OptiTrust is open source, and open to collaboration.
Don't hesitate to get in touch with Arthur Charguéraud or Thomas Koehler.

Publications

Case Studies

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.
  • 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.

Funding

  • ANR OptiTrust: from October 2022 to September 2026, 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.
  • 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.