Kayvan Memarian

I am a research associate with Peter Sewell working on the Cerberus C semantics (github repo), an executable model formalising the C programming language and its memory object model.

Previously, I worked on relaxed-memory concurrency.

Contact details

email:    kayvan.memarian cl.cam.ac.uk
office:   FS14
address:  University of Cambridge
          Computer Laboratory
          15 JJ Thomson Avenue
          Cambridge, CB3 0FD

Publications

• [14] A CHERI C Memory Model for Verified Temporal Safety
  Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Filardo, Ian Stark, and Peter Sewell.
  In CPP 2025.

• [13] Fulminate: Testing CN Separation-Logic Specifications in C
  Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte, Neel Krishnaswami, and Peter Sewell.
  In POPL 2025.

• [12] Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance
  Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alex Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, and Peter Sewell.
  In ASPLOS 2024.

• [11] CN: Verifying Systems C Code with Separation-Logic Refinement Types
  Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami.
  In Proc. 50th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2023).

• [10] VIP: Verifying Real-World C Idioms with Integer-Pointer Casts
  Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell.
  In Proc. 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022).

• [9] RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types (project page)
  Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg.
  In Proc. 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021).

• [8] Cerberus-BMC: a Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C
  Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean Pichon-Pharabod, and Peter Sewell.
  In Proc. 31st International Conference on Computer-Aided Verification (CAV 2019).

• [7] Exploring C Semantics and Pointer Provenance (supplement)
  Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell.
  In Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019).

• [6] An operational semantics for C/C++11 concurrency (supplement)
  Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell.
  In SPLASH 2016 OOPSLA.

• [5] Into the Depths of C: Elaborating the De Facto Standards
  Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson and Peter Sewell.
  In Proc. 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016).

• [4] The Problem of Programming Language Concurrency Semantics
  Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod and Peter Sewell.
  In Proc. 24th European Symposium on Programming (ESOP 2015).

• [3] An Axiomatic Memory Model for Power Multiprocessors (supplement | bibtex)
  Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo Martin, Peter Sewell and Derek Williams.
  In Proc. 24th International Conference on Computer Aided Verification (CAV 2012).

• [2] Synchronising C/C++ and POWER (supplement | bibtex)
  Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave and Derek Williams.
  In Proc. 33rd ACM SIGPLAN conference on Programming language design and implementation (PLDI 2012).

• [1] Clarifying and compiling C/C++ concurrency: from C++0x to POWER (supplement | bibtex)
  Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar and Peter Sewell.
  In Proc. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012).

PhD thesis

Supervisions

• 2012 - Lent: Hoare Logic (II), Complexity Theory (IB)
• 2013 - Lent: Computation Theory (IB)
• 2014 - Lent: Hoare Logic (II); Michaelmas: Type Theory (II)
• 2015 - Lent: Computation Theory (IB)