David Monniaux
where else to find them
what they talk about
all 5 in the filters
where they keep going back
all 4 in the filters
on a stage with
all 18 in the filters
who talks about the same things
- Sylvain Boulmé4 talks
- Benjamin Bonneau2 talks
- Thomas Bourgeat9 talks
- Armaël Guéneau7 talks
- Adam Chlipala23 talks
- Vivek Sarkar7 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… | ||
| Short talks: Past, Present and Future of AI | N40AI 2024 | 2024-01-20 |
A rapid history of abstract interpretation that traces concrete claims and engineering outcomes: presents the formal method used to analyze Airbus C code with… | ||
| Memory simulations, security and optimization in a verified compiler | CPP 2024 | 2024-01-15 |
CompCert receives three new, machine-checked transformations: implemented and proved stack canaries and pointer authentication as security inserts, and a… | ||
| 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… | ||
| Data Abstraction: A General Framework to Handle Program Verification of Data Structures | SAS 2021 | 2021-10-17 |
Proposes a constructive reduction that turns universally quantified array properties like “all elements below index i are nonzero” into a purely scalar… | ||
| 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 | ||