Ben Simner

A complete BibTeX bibliography can be found here [raw].

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.

Grants / Awards

• Amazon Research Award
  Gradual Lightweight Methods for High-Assurance Cloud Infrastructure. Automated Reasoning, Fall 2025. $79,996.00 cash award plus $10,000 in AWS credits.
  Peter Sewell (PI), Ben Simner (co-author), Kayvan Memarian (co-author), Rini Banerjee (co-author), Hiroyuki Katsura (co-author).
• ERC Proof-of-Concept Grant
  ELVER-CHECK: Well-grounded Lightweight Assurance for Critical Systems Software. 2024. ERC-2024-POC/101189371. €150,000.
  Peter Sewell (PI), Ben Simner (co-author), Kayvan Memarian (co-author), Jean Pichon-Pharabod (co-author).
• Amazon Research Award
  The Foundations of Cloud Virtual-machine Isolation. Automated Reasoning, Fall 2023. $54,603 cash award plus $20,000 in AWS credits.
  Peter Sewell (PI), Ben Simner (co-author).

Dissertations

• Arm systems semantics. [pdf] [bib] [doi] [Cambridge repository] [errata]
  Ben Simner. PhD thesis. University of Cambridge, April 2025.
• Rufous: Automated comparison of implementations of purely functional data structures. [pdf] [bib]
  Ben Simner. MEng dissertation. University of York, 2018.

Presentations

• Precise Exceptions in Relaxed Architectures. [slides]
  Presented at the 52nd International Symposium on Computer Architecture, Tokyo, Japan, 23rd June 2025.
• Arm System Semantics. [slides]
  Presented at the Big Specification workshop at the Isaac Newton Institute, Cambridge, UK, 10th October 2024.
• Reasoning about relaxed systems. [slides]
  Presented at the Future of Weak Memory workshop at POPL'24, London, UK, 15th January 2024.
• Relaxed Virtual Memory. [slides]
  Presented at Aarhus University to the Logic and Semantics research group, Aarhus, Denmark, 5th December 2022.
• Automated comparison of purely functional data structures. [slides]
  Presented at the University of Kent, Programming Languages and Semantics seminar series, Kent, 12th September 2022.
• Relaxed Virtual Memory Semantics. [slides] [video]
  Presented at the Newton institute Cambridge, 11th August 2022.
• Relaxed Virtual Memory. [slides]
  Presented in ESOP at ETAPS, Munich, 6th April 2022.
• Modelling Systems Architecture. [slides]
  Presented at the Arm Research Summit, Austin Texas, September 2019.
• Relaxed Systems Architecture: Instruction Fetching. [slides]
  Presented as an LFCS Seminar, Edinburgh, February 2020.
• Rufous: automated data structure selection. [slides]
  Presented at the University of York, 2018.
• Microsoft Excel: A PL Perspective. [slides]
  Presented at the University of York, 2017.

Posters

• Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor. [pdf]
  Presented at the 31st Symposium on Operating Systems Principles, Seoul, Republic of Korea, 14th October 2025.
• Precise Exceptions in Relaxed Architectures. [pdf]
  Presented at the 52nd International Symposium on Computer Architecture, Tokyo, Japan, 23rd June 2025.

Miscellaneous files

• ARMv8-A System Semantics: iFlat Operational Model. 2019.
• ARMv8-A System Semantics: iFlat Axiomatic Model. 2019.

Drafts

• [drafts]