Benjamin Gregoire
where else to find them
what they talk about
where they keep going back
no series more than once — all 4 in the filters
on a stage with
all 10 in the filters
who talks about the same things
- Martin Avanzini4 talks
- Gilles Barthe17 talks
- Gabriele Vanoni7 talks
- Georg Moser5 talks
- Benjamin Lucien Kaminski14 talks
- Joost-Pieter Katoen14 talks
| title | conference | date |
|---|---|---|
| Preservation of Speculative Constant-time by Compilation | PriSC 2025 (with POPL 2025) | 2025-01-20 |
Shows that common compilers (GCC -O0 and -O1 and Jasmin) produce speculatively insecure binaries from speculatively constant-time sources, then builds a… | ||
| Preservation of speculative constant-time by compilation | POPL 2025 | 2025-01-19 |
Shows that mainstream compilers (GCC -O0/-O1 and Jasmin) can break speculative constant-time by removing or introducing Spectre-v1 leaks, gives concrete… | ||
| A quantitative probabilistic relational Hoare logic | POPL 2025 | 2025-01-19 |
eRHL is a program logic whose pre/post-conditions are nonnegative real-valued functions on pairs of states, and it gives upper bounds on expectations… | ||
| Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security(…) | OOPSLA 2024 | 2024-10-20 |
Proposes a EHL + pRHL hopping rule that reduces expectation-based proof goals to related programs, implements it inside EasyCrypt integration, and proves… | ||
| Practical and sound equality tests, automatically | CPP 2023 | 2023-01-16 |
A tool called feqb synthesizes sound equality tests and correctness proofs for Coq inductive types used with the Mathematical Components library, handling very… | ||
| nothing matches | ||