• ArchSem: Reusable rigorous semantics of relaxed architectures. Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Zongyuan Liu, Nils Lauermann, Alasdair Armstrong, and Peter Sewell. In POPL 2026. [ bib | doi | pdf | github | abstract ]
• Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor. Kayvan Memarian, Ben Simner, David Kaloper-Meršinjak, Thibaut Pérami, and Peter Sewell. In SOSP 2025. [ bib | doi | pdf | abstract ]
• Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture. Angus Hammond, Ricardo Almeida, Thomas Bauereiss, Brian Campbell, Ian Stark, and Peter Sewell. In PLDI 2025. [ bib | doi | pdf | abstract ]
• Precise exceptions in relaxed architectures. Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, and Peter Sewell. In ISCA 2025, Best paper award. [ bib | doi | errata | pdf | abstract ]
• ISO/IEC TS 6010:2025 Programming languages --- C --- A provenance-aware memory object model for C, ISO/IEC JTC 1/SC 22. ISO, May 2025. Based on N3005: A Provenance-aware Memory Object Model for C. Working Draft Technical Specification ISO/IEC TS 6010:2023 (E). Jens Gustedt, Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Martin Uecker. http://www.open-std.org/jtc1/sc22/wg14/www/docs/n3005.pdf. June 2022. [ bib | .html | abstract ]
• Arm systems semantics. Ben Simner. PhD thesis, University of Cambridge, April 2025. [ bib | doi | errata | pdf | http | abstract ]
• Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor, Louis-Emile Ploix, Alasdair Armstrong, Tom Melham, Ray Lin, Haolong Wang, and Anastasia Courtney, February 2025. [ bib | arXiv | http | abstract ]
• Towards general white-box automation: a typeclass-guided context cleaner. Thibaut Pérami. In CoqPL 2025. [ bib | http ]
• A CHERI C Memory Model for Verified Temporal Safety. Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Wesley Filardo, Ian Stark, and Peter Sewell. In CPP 2025. [ bib | doi | http ]
• It Is Time to Standardize Principles and Practices for Software Memory Safety. Robert N.M. Watson, John Baldwin, David Chisnall, Tony Chen, Jessica Clarke, Brooks Davis, Nathaniel Filardo, Brett Gutstein, Graeme Jenkinson, Ben Laurie, Alfredo Mazzinghi, Simon Moore, Peter G. Neumann, Hamed Okhravi, Alex Richardson, Alex Rebert, Peter Sewell, Laurence Tratt, Murali Vijayaraghavan, Hugo Vincent, and Konrad Witaszczyk. Communications of the ACM, 68(2):40–45, January 2025. [ bib | doi | http | abstract ]
• Fulminate: Testing CN Separation-Logic Specifications in C. Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte, Neel Krishnaswami, and Peter Sewell. In POPL 2025. [ bib | doi | pdf | abstract ]