sise sycomores

The Chamois project: improvements to CompCert

November 23, 2026 at 10:30 AM

David Monniaux

Abstract:

CompCert is one of the very few realistic formally verified compilers,
and the only one for C. It however lacks some features (for
performance and security) commonly found in other compilers.

The Chamois project aims at bringing these to CompCert.

“How far can we go in a formally proved fashion?”

Joint work with Sylvain Boulmé and our students (Cyril Six, Léo Gourdin, Alexandre Bérard, Benjamin Bonneau)

More...

Salle Turquoise, 4ème étage, bât ESPRIT

Agenda scientifique

Voir l'agenda complet »

• ToPSyS Seminars

  Achille Melingui et Yehya Sharif November 12, 2026 at 2 PM

• ToPSyS Seminar

  Mohd Faizan November 19, 2026 at 2 PM

• Séminaire Axe IA

  Mathilde Lepers November 20, 2026 at 2 PM

• Seminar

  David Monniaux November 23, 2026 at 10:30 AM

• SOFA WEEK 2026

  from November 23 to 27, 2026

• GeoGen3DHuman Workshop

  Tolga Birdal, Gül Varol et Eric Paquet November 24, 2026 at 9 AM

• Systems & Control Seminar

  Ivan Yupanqui Tello November 25, 2026 at 10 AM

• Colloquium Polaris

  Pierre Marquis November 26, 2026 at 2 PM

• Technical Seminars PADR

  from November 30 to December 7, 2026

• Portes ouvertes FR SCV

  December 1, 2026 at 9 AM

• Colloquium Polaris

  Etienne Ollion December 15, 2026 at 2 PM

• Colloquium Polaris

  Clémentine Maurice January 28, 2027 at 2 PM

• Workshop

  Klaus Dolag et Jenny Sorce from March 8 to 12, 2027

• Colloquium Polaris

  Nathanael Fijalkow March 25, 2027 at 2 PM

• Colloquium Polaris

  Marion Monnet May 27, 2027 at 2 PM

• Colloquium Polaris

  Patrick Bas June 24, 2027 at 2 PM

Defenses

• Théo Gueuret (thesis)

  November 12, 2026 at 9 AM

• Mohammed Boudaoud (thesis)

  December 8, 2026 at 10 AM