Aseem Rastogi
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 Podelski3 editions2022–2026
all 4 in the filters
on a stage with
all 31 in the filters
who talks about the same things
- Nikhil Swamy14 talks
- Danel Ahman7 talks
- Guido Martínez10 talks
- Aymeric Fromherz9 talks
- Cătălin Hriţcu16 talks
- Kartik Nagar6 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… | ||
| Automatically Verifying Replication-aware Linearizability | OOPSLA 2025 | 2025-10-16 |
Automated verification framework proves replication-aware linearizability for Mergeable Replicated Data Types by checking novel algebraic laws on the three-way… | ||
| 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… | ||
| Hardening Attack Surfaces with Formally Proven Binary Format Parsers | PLDI 2022 | 2022-06-13 |
A toolchain converts a descriptive 3D format into F proofs and then to C, yielding memory- and integer-safe parsers with functional correctness and… | ||
| SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed ... | ICFP 2020 | 2020-08-23 |
SteelCore provides a semantics for CSL inside F, deriving Hoare rules from effectful non‑deterministic interleaving; it encodes computations as action trees… | ||
| nothing matches | ||