Tahina Ramananandro
where else to find them
no profile links on file
what they talk about
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2025–2026
on a stage with
all 30 in the filters
who talks about the same things
- Guido Martínez10 talks
- Nikhil Swamy14 talks
- Gabriel Ebner6 talks
- Aseem Rastogi7 talks
- Danel Ahman7 talks
- Cătălin Hriţcu16 talks
| title | conference | date |
|---|---|---|
| Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic | PLDI 2026 | 2026-06-15 |
Kuiper is an F library that uses Pulse-based separation logic to verify GPU kernels, extending the logic with forall+ connective and located resources to model… | ||
| 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… | ||
| PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs | PLDI 2025 | 2025-06-16 |
PulseCore is a new, mechanized concurrent separation logic implemented inside F★ that claims to support impredicative invariants and higher‑order ghost state… | ||
| FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores | CPP 2023 | 2023-01-16 |
FastVer2 is a verified, concurrent monitor for the Faster key-value store: implemented in C (≈8,000 lines produced from ≈50,000 lines of F proofs) using the… | ||
| 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… | ||
| Everparse: A Verifying Compiler from Data Format Specifications to Verified Efficient Parsers | PriSC 2020 | 2020-01-25 |
A verified compiler that takes dependent data-format descriptions and emits F specifications plus Low implementations extracted to high-performance C, with… | ||
| nothing matches | ||