Computer Scientist at the University of Cambridge, UK. Researching tools and techniques for testing low-level software, architectural multiprocessor semantics, and verification of concurrent programs, as part of the REMS project.
Keywords: Programming Languages & Semantics ∙ Computer Architecture ∙ Systems ∙ Concurrency ∙ Testing ∙ Verification
Publications
-
Precise exceptions in relaxed architectures.
[pdf]
[bib]
[doi]
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean-Pichon Pharabod, and Peter Sewell. (to appear) ISCA 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.