Kayvan Memarian
where else to find them
what they talk about
all 5 in the filters
where they keep going back
- POPL3 editions2022–2025
all 4 in the filters
on a stage with
all 20 in the filters
who talks about the same things
- Christopher Pulte4 talks
- Rini Banerjee2 talks
- Peter Sewell14 talks
- Dhruv C. Makwana3 talks
- Neel Krishnaswami10 talks
- Michael Sammler16 talks
| title | conference | date |
|---|---|---|
| Combining Agentic AI and Lightweight Formal Methods To Find Bugs in a Production(…) | PAgE 2026 | 2026-06-15 |
Combines the executable-spec framework for Android pKVM with an OpenAI Codex-based agent that writes ambient-C ghost code and tests, running for about one… | ||
| Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…) | PLDI 2026 | 2026-06-15 |
Integrates CN separation logic into runtime checks, unit and SMT-based random generator testing, and final machine-checked proofs, all on the real-world PKVM… | ||
| A CHERI C Memory Model for Verified Temporal Safety | CPP 2025 | 2025-01-20 |
Defines a CHERI C object memory model that implements a new PNVI-CHERI provenance scheme, encodes five revocation strategies, and plugs into the Cerberus… | ||
| Fulminate: Testing CN Separation-Logic Specifications in C | POPL 2025 | 2025-01-19 |
Fulminate translates CN separation-logic annotations into executable C checks that enforce ownership ghost state and explicit ownership transfer at runtime… | ||
| CN: Verifying Systems C Code with Separation-Logic Refinement Types | POPL 2023 | 2023-01-15 |
CN is a separation-logic refinement type system for ISO C that uses a Cerberus translation to a core language, implements resource types as first-class… | ||
| VIP: Verifying Real-World C Idioms with Integer-Pointer Casts | POPL 2022 | 2022-01-16 |
Presents VIP, a memory-object model that proves compatible with PNVI while making integer→pointer casts verifiable by adding an explicit provenance-copying… | ||
| nothing matches | ||