Le LMF participera prochainement à un meetup Rust Paris le 9 juin 2026 avec une présentation consacrée à Creusot, son outil de vérification formelle de programmes Rust.
Le LMF, lauréat de VerifyThis 2026, présentera Creusot à Rust Paris
Le LMF participera prochainement à Rust Paris 2026 le 9 juin 2026 avec une présentation consacrée à Creusot, son outil de vérification formelle de programmes Rust.
Lors de cette présentation, Li-yao Xia (ingénieur R&D) et Jacques-Henri Jourdan (chargé de recherche) expliqueront comment Creusot permet de prouver l’absence de certaines classes d’erreurs dans les programmes Rust grâce à la vérification déductive. Cette approche repose sur l’écriture de contrats de fonctions, c’est-à-dire de spécifications formelles décrivant précisément le comportement attendu des fonctions. L’exposé présentera également plusieurs études de cas de bibliothèques et d’applications vérifiées avec Creusot.
Cet événement fait suite à un résultat majeur obtenu lors de VerifyThis 2026, le concours international de vérification de programmes organisé à Turin dans le cadre d’ETAPS. Parmi 24 équipes participantes, Li-yao Xia et Jacques-Henri Jourdan ont reçu le prix de la Best Overall Team. Le LMF a également été distingué avec le prix de la Best One-Person Team, décerné à Jean-Christophe Filliâtre.
Ces résultats soulignent à la fois la qualité des travaux du LMF en vérification formelle et l’importance croissante de Creusot.