Publications
-
Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor.
[pdf]
[bib]
[doi]
Kayvan Memarian, Ben Simner, David Kaloper-Meršinjak, Thibaut Pérami, and Peter Sewell. SOSP 2025. -
Precise exceptions in relaxed architectures.
[pdf]
[bib]
[doi]
[errata]
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean-Pichon Pharabod, and Peter Sewell. ISCA 2025. Best Paper Award -
Arm systems semantics.
[pdf]
[bib]
[doi]
[Cambridge repository]
[errata]
Ben Simner. PhD thesis. University of Cambridge, April 2025. -
Wait-Free Weak Reference Counting.
[pdf]
[bib]
[doi]
Matthew J. Parkinson, Sylvan Clebsch, and Ben Simner. ISMM 2023. -
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (Journal version).
[pdf]
[bib]
[doi]
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte and Peter Sewell. Formal Methods in System Design, May 2023. -
Relaxed virtual memory in Armv8-A.
[pdf]
[extended pdf]
[bib]
[doi]
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, and Peter Sewell. ESOP 2022. -
Isla: Integrating Full-Scale ISA Semantics and Axiomatic
Concurrency Models.
[pdf]
[extended pdf]
[bib]
[doi]
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte and Peter Sewell. CAV 2021. -
ARMv8-A system semantics: instruction fetch in
relaxed architectures.
[pdf]
[extended pdf]
[bib]
[doi]
[errata]
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell. ESOP 2020. -
Starling: Lightweight Concurrency Verification with
Views.
[pdf]
[bib]
[doi]
Matt Windsor, Mike Dodds, Ben Simner, and Matthew J Parkinson. Computer Aided Verification 2017.
See /research/ for copies of presentations, a complete bibliography, and other documents including drafts.