Cédric Fournet
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2022–2026
all 5 in the filters
on a stage with
all 49 in the filters
who talks about the same things
- Cătălin Hriţcu16 talks
- Danel Ahman7 talks
- Exequiel Rivas6 talks
- Aseem Rastogi7 talks
- Guido Martínez10 talks
- Karthikeyan Bhargavan5 talks
| title | conference | date |
|---|---|---|
| Project Everest: Perspectives from Developing Industrial-Grade High-Assurance(…) | PLDI 2026 | 2026-06-15 |
Project Everest produces a verified TLS stack and crypto suite rather than promises: it yields 1.3 million lines of F source that build in two hours, emits… | ||
| Confidential Computing within an AI Accelerator | USENIX ATC '23 | 2023-07-10 |
Built an AI accelerator extension called IPU Trusted Extensions (ITX) that adds an on‑chip hardware root-of-trust and PCIe Gen4‑rate cryptographic engines… | ||
| ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER | CPP 2023 | 2023-01-16 |
Claims a first formalization of ASN.1 DER with a mechanized proof of non-malleability and a verified compiler in F that uses the EverParse framework to produce… | ||
| Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris | PLDI 2022 | 2022-06-13 |
Built on Iris, Diaframe provides a foundational yet automated verifier for fine‑grained concurrency, using syntax‑directed rule versions, goal‑directed proof… | ||
| IA-CCF: Individual Accountability for Permissioned Ledgers | 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22) | 2022-04-04 |
A permissioned ledger implementation called IA-CCF signs and logs BFT protocol messages into the ledger and issues Merkle-tree receipts that clients can audit… | ||
| Oblivious Multi-Party Machine Learning on Trusted Processors | USENIX Security '16 | 2016-08-10 |
Framework uses real Intel SGX (Skylake) enclaves and a library of data-oblivious primitives plus an oblivious batch shuffling sampler to prevent cache-line… | ||
| nothing matches | ||