Sylvain Boulmé
where else to find them
no profile links on file
what they talk about
where they keep going back
on a stage with
all 9 in the filters
who talks about the same things
- David Monniaux7 talks
- Benjamin Bonneau2 talks
- Vivek Sarkar7 talks
- Jun Shirako3 talks
- Thomas Bourgeat9 talks
- Armaël Guéneau7 talks
| title | conference | date |
|---|---|---|
| Formally verified hardening of C programs against hardware fault injection | CPP 2025 | 2025-01-20 |
Implements two control-flow hardening transforms over CompCert RTL and proves two properties in Coq proofs: semantic preservation (no behavior change without… | ||
| Formally Verifying Optimizations with Block Simulations | OOPSLA 2023 | 2023-10-23 |
Framework implements block-level forward simulations inside CompCert and proves validators in the Coq proof assistant that check concrete morphisms between… | ||
| Formally Verified Superblock Scheduling | CPP 2022 | 2022-01-17 |
A certified scheduler that actually runs over superblocks is implemented and hooked into CompCert integration with a machine-checked semantic preservation… | ||
| Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors | OOPSLA 2020 | 2020-11-15 |
Implements a post-pass instruction scheduler for CompCert targeting the Kalray Coolidge VLIW and ships an untrusted OCaml scheduler plus a Coq-verified… | ||
| nothing matches | ||