Karthikeyan Bhargavan
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2022–2026
all 4 in the filters
on a stage with
all 27 in the filters
who talks about the same things
- Cătălin Hriţcu16 talks
- Chris Hawblitzel9 talks
- Exequiel Rivas6 talks
- Cédric Fournet7 talks
- Danel Ahman7 talks
- Ranjit Jhala19 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… | ||
| Software Verification meets Real-World Cryptography | Dafny 2026 | 2026-01-11 |
Verified cryptography is now practical: about a dozen verified libraries exist and verified code runs in Firefox and on major cloud services, produced from… | ||
| A Mechanically Verified Garbage Collector for OCaml | OCaml Workshop 2025 | 2025-10-17 |
Verified stop‑the‑world mark‑and‑sweep GC implemented from scratch, mechanized in F with its low‑level subset Low and extracted to C via KaRaMel, then linked… | ||
| Keynote: Towards High-Assurance Cryptographic Software | RuhrSec 2023 | 2023-05-11 |
Formal verification and security-oriented languages are used end-to-end: mechanized proofs (ProVerif, Tamarin, F, EasyCrypt) validate protocol designs like… | ||
| Checking Robustness to Weak Persistency Models | PLDI 2022 | 2022-06-13 |
PSign dynamically checks whether a program running under the x86 weak persistency model behaves as if it ran under strict persistency by constructing… | ||
| nothing matches | ||