Ben Simner - All Publications

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.

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.