• The Cerberus C semantics. Kayvan Memarian. Technical Report UCAM-CL-TR-981, University of Cambridge, Computer Laboratory, May 2023. PhD thesis. [ bib | doi | .pdf | abstract ]
• RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types. Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. In PLDI 2021. [ bib | pdf | abstract ]