Ben Simner - All Publications

Relaxed virtual memory in Armv8-A. [pdf] [extended pdf] [bib]
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]
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]
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell. ESOP 2020.
Rufous: Automated comparison of implementations of purely functional data structures. [pdf] [bib]
Ben Simner. (MEng) University of York, 2018.
Starling: Lightweight Concurrency Verification with Views. [pdf] [bib]
Matt Windsor, Mike Dodds, Ben Simner, and Matthew J Parkinson. Computer Aided Verification 2017.

A complete BibTeX compatible bibliography can be found here.

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.