Sylvain BOULME

Last works: formally verified defensive programming with Coq and OCaml

Chamois Arsene a variant of Chamois CompCert (see below) with Formally Verified Hardening of C Programs against Hardware Fault Injection, an CPP'25 paper, by Pesin, Boulmé, Monniaux and Potet.
Formally Verified Optimizations in the Chamois CompCert Compiler, joint works with D. Monniaux, L. Gourdin, B. Bonneau, A. Bérard, C. Six and students.
Main papers:
- Formally Verifying Optimizations with Block Simulations, an OOPSLA'23 paper, by Gourdin, Bonneau, Boulmé, Monniaux and Bérard.
- Certified and Efficient Instruction Scheduling, an OOPSLA'20 paper, by Six, Boulmé and Monniaux.
Click-this to expand/collapse the 5-minutes presentation by C. Six on Formally Verified Instruction Scheduling
Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles), my habilation thesis (HDR), defended on September 27, 2021.
Certifying Answers of Boolean 2018 SAT-Solvers (joint work with T. Thomas Vandendorpe) with the Impure library.
The Verified Polyhedra Library (source code on github), a joint work with Alexis Fouilhé, Alexandre Maréchal, David Monniaux, Michaël Périn and Hang Yu.
- A Coq Tactic for Equality Learning in Linear Arithmetic.
- A refinement calculus for certification of computations on abstract domains in Coq: this is a joint work with Alexandre Maréchal and Michaël Périn.
- A certifying frontend for (sub)polyhedra abstract domains: the first version of the Coq frontend for the VPL written with Alexis Fouilhé.

Labo: Verimag
Area: Proofs of programs, Formal methods, Semantics of programming languages, Verified compilation.
Formalisms: Abstract Interpretation, Refinement calculus, Type theory.
Issues: Combination of programming paradigms, Refinement, Modularity, Inheritance, Parametricity, Applications of dependent types, Certification of verification tools, Result (or lightweight) certification.
Related Tools: OCaml, Coq, CompCert, Verasco, Frama-C, Why, Rust and Creusot, Atelier B, FoCaLiZe, Lucid Synchrone,
Previous works using Coq:
- FoCaLiZe: specifying, programming and proving Computer Algebra libraries.
- Lucid Synchrone in Coq: a synchronous denotational semantics for synchronous programming languages in type theory.
- Higher-order refinement calculus
- A very small tutorial on Hoare Logic: Online description or sources and documentation.
- A tiny tutorial on Simply Typed Lambda-Mu Calculus (Curry-Howard in classical propositional logic): Online description or source file.

Lieu: l'Ensimag.

Projet GL (Ensimag 1A Apprentissage et Ensimag 2A).
Grammaires et compilation (Ensimag 1A Apprentissage).
Théorie des langages (Ensimag 1A).
Analyse de code pour la sûreté et la sécurité (Ensimag 2A):
- Intro à CompCert et Coq
Program Testing and Verification (Mosig 2):
- Tutorial on Frama-C WP and intro to Hoare Logic