• VIP: Verifying Real-World C Idioms with Integer-Pointer Casts. Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, and Peter Sewell. In POPL 2022, Proc. ACM Program. Lang. 6, POPL, Article 20. [ bib | doi | supplementary material | project page | pdf | abstract ]
• 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 CAV 2019. [ bib | project page | pdf | abstract ]
• Exploring C Semantics and Pointer Provenance. Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 67. Also available as ISO/IEC JTC1/SC22/WG14 N2311. [ bib | doi | supplementary material | project page | pdf | abstract ]
• An operational semantics for C/C++11 concurrency. Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell. In OOPSLA 2016. [ bib | doi | pdf | http | abstract ]
• 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 PLDI 2016, PLDI 2016 Distinguished Paper award. [ bib | doi | project page | pdf | http | abstract ]