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.