Thomas Bourgeat
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
no series more than once — all 9 in the filters
on a stage with
all 20 in the filters
who talks about the same things
- Adam Chlipala23 talks
- Clément Pit-Claudel17 talks
- Kathleen Fisher9 talks
- Matthieu Sozeau14 talks
- Thomas Reps20 talks
- Samuel Gruetter5 talks
| title | conference | date |
|---|---|---|
| Towards composable proofs of cache coherence protocols | CPP 2026 | 2026-01-12 |
Proposes a compositional proof that MSI refines the combination of MI and SI, formalized in Lean 4, cutting required invariants from hundreds to just 15 by… | ||
| Save what must be saved: Secure context switching with Sailor | USENIX Security '25 | 2025-08-13 |
Sailor uses the machine‑readable Sail ISA and the Isla symbolic executor to generate instruction traces (about 3 GB traces, 20 hours symbolic execution) and an… | ||
| Making Concurrent Hardware Verification Sequential | PLDI 2025 | 2025-06-16 |
Introduces Fjfj, a Bluespec-like language that removes exponential proof cases by separating action methods vs value methods and forbidding multiple action… | ||
| Performance Interfaces for Hardware Accelerators | 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) | 2024-07-10 |
Proposes a precise accelerator performance IR called LPN and an open toolchain ltc that converts RTL-derived IR into executable performance interfaces and… | ||
| Flexible Instruction-Set Semantics via Abstract Monads | ICFP 2023 | 2023-09-04 |
Claims a single Haskell-based core semantics, parameterized by a Risk5Machine type class over monads, supports testing, interactive proof, model checking and… | ||
| Hardware Verification of Timing Side Channel Freedom in the Spectre Era | PLARCH 2023 | 2023-06-17 |
Claim: a synthesizable, pipelined two-core RISC-V design plus a hardware security monitor enforces strong timing isolation and is proven equivalent to an… | ||
| An experience report on writing usable DSLs in Coq | CoqPL 2021 | 2021-01-19 |
A hardware DSL called koika is implemented as a deeply embedded AST in Coq with a few thousand lines of code and hundreds of lines of notations; usability… | ||
| An experience report on writing usable DSLs in Coq | POPL 2021 | 2021-01-17 |
A report on building a hardware DSL in Coq: the codebase totals a few thousand lines of Coq and hundreds of lines of notations; Coq 8.9 custom entries let the… | ||
| Formal Specification | 8th RISC-V Workshop Barcelona 2018 | 2018-05-07 |
Formal RISC‑V semantics implemented as a configurable, monadic Haskell monadic spec that leaves low‑level ops (get/set reg, memory I/O) abstract so the same… | ||
| nothing matches | ||