An Axiomatic Memory Model for POWER Multiprocessors. - Sela Mador-Haim; Luc Maranget; Susmit Sarkar; Kayvan Memarian; Jade Alglave; Scott Owens; Rajeev Alur; Milo M. K. Martin; Peter Sewell; Derek Williams (CAV, 2012)

Synchronising C/C++ and POWER. - Susmit Sarkar; Kayvan Memarian; Scott Owens; Mark Batty; Peter Sewell; Luc Maranget; Jade Alglave; Derek Williams (PLDI, 2012)

Clarifying and compiling C/C++ concurrency: from C++11 to POWER. - Mark Batty; Kayvan Memarian; Scott Owens; Susmit Sarkar; Peter Sewell (POPL, 2012)

The Problem of Programming Language Concurrency Semantics. - Mark Batty; Kayvan Memarian; Kyndylan Nienhuis; Jean Pichon-Pharabod; Peter Sewell (ESOP, 2015)

An operational semantics for C/C++11 concurrency. - Kyndylan Nienhuis; Kayvan Memarian; Peter Sewell (OOPSLA, 2016)

Into the depths of C: elaborating the de facto standards. - Kayvan Memarian; Justus Matthiesen; James Lingard; Kyndylan Nienhuis; David Chisnall; Robert N. M. Watson; Peter Sewell (PLDI, 2016)

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; Peter Sewell (CAV (1), 2019)

Exploring C semantics and pointer provenance. - Kayvan Memarian; Victor B. F. Gomes; Brooks Davis; Stephen Kell; Alexander Richardson 001; Robert N. M. Watson; Peter Sewell (Proc. ACM Program. Lang., 2019)

RefinedC: automating the foundational verification of C code with refined ownership types. - Michael Sammler; Rodolphe Lepigre; Robbert Krebbers; Kayvan Memarian; Derek Dreyer; Deepak Garg 001 (PLDI, 2021)

VIP: verifying real-world C idioms with integer-pointer casts. - Rodolphe Lepigre; Michael Sammler; Kayvan Memarian; Robbert Krebbers; Derek Dreyer; Peter Sewell (Proc. ACM Program. Lang., 2022)

CN: Verifying Systems C Code with Separation-Logic Refinement Types. - Christopher Pulte; Dhruv C. Makwana; Thomas Sewell; Kayvan Memarian; Peter Sewell; Neel Krishnaswami (Proc. ACM Program. Lang., 2023)

Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance. - Vadim Zaliva; Kayvan Memarian; Ricardo Almeida 003; Jessica Clarke 001; Brooks Davis; Alexander Richardson 001; David Chisnall; Brian Campbell 001; Ian Stark; Robert N. M. Watson; Peter Sewell (ASPLOS (1), 2024)

A CHERI C Memory Model for Verified Temporal Safety. - Vadim Zaliva; Kayvan Memarian; Brian Campbell 001; Ricardo Almeida 003; Nathaniel Wesley Filardo; Ian Stark; Peter Sewell (CPP, 2025)

Fulminate: Testing CN Separation-Logic Specifications in C. - Rini Banerjee; Kayvan Memarian; Dhruv C. Makwana; Christopher Pulte; Neel Krishnaswami; Peter Sewell (Proc. ACM Program. Lang., 2025)