Kayvan Memarian -

Registered user since Fri 19 Dec 2014

Name:Kayvan Memarian

Affiliation:University of Cambridge

Personal website: https://www.cl.cam.ac.uk/~km569

Contributions

2026

PAgE

Author of Combining Agentic AI and Lightweight Formal Methods To Find Bugs in a Production Hypervisor within the PAgE 2026-track

PLDI

Author of Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows within the PLDI Research Papers-track

POPL

Committee Member in Program Committee within the POPL-track

TPSA

Author of Gradually Retrofitting Assurance into Systems Software: A Separation-Logic Approach within the TPSA 2026-track

2025

POPL

Author of Fulminate: Testing CN Separation-Logic Specifications in C within the POPL-track

CPP

Author of A CHERI C Memory Model for Verified Temporal Safety within the CPP 2025-track

2023

POPL

Author of CN: Verifying Systems C Code with Separation-Logic Refinement Types within the POPL-track

2022

PLDI

Author of (PLDI 2021) RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types within the SIGPLAN Track-track

POPL

Author of VIP: Verifying Real-World C Idioms with Integer-Pointer Casts within the POPL-track

WITS

Author of CN: A Refinement Type System for C within the WITS 2022-track

2021

PLDI

Author of RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types within the PLDI-track

2020

DeepSpec

Presenter of Cerberus: executable reference semantics and memory object models for ISO and de facto C within the REMS-DeepSpec 2020-track

2019

POPL

Author of Exploring C Semantics and Pointer Provenance within the Research Papers-track

2016

SPLASH

Author of An Operational Semantics for C/C++11 Concurrency within the OOPSLA-track

PLDI

Author of Into the depths of C: elaborating the de facto standards within the Research Papers-track

2015

ESOP

Author of The Problem of Programming Language Concurrency Semantics within the ESOP-track