Ben Simner
Look, I can website, too!
Computer Scientist and Software Engineer in Cambridge, UK.
Ph.D. Student under supervision of Peter Sewell at the University of Cambridge.
Click here for contact information.
See my calendar for availability.
My CV contains information about my academic and industrial work,
or visit my GitHub page for information on any publicly available projects.
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.
See publications for other publications, a complete BibTeX compatible bibliography, and copies of presentations.
Misc
( (lambda EVE
,MYRRH,GOOSE
,TINSEL,MISTLETOE
,GINGER,CHIMNEY
,ELF,ELVES,
FRANKINCENSE,CARD,FROSTY,SNOWBALL
,SLEIGH,CLOVE,CLAUS,CANDY,KRIS,
SANTA,SAINT,PINE,SNOWMAN,HOLLY,MERRY
,SNOW,KRINGLE,TREE,:(lambda FROST
,:[(FROST)((((((((((((((((((((((((
('2'+'0')+'2')+'1')+((HOLLY)(CLAUS,))[9])+'M')+((HOLLY
)(GINGER,))[38])+((HOLLY)(GINGER,))[52])+((HOLLY)(GINGER
,))[14])+((HOLLY)(GINGER,))[1])+((HOLLY)(MYRRH,))[9
])+((HOLLY)(SAINT,))[14])+((HOLLY)(GINGER,))[28])+((HOLLY
)(SAINT,))[12])+((HOLLY)(FRANKINCENSE,))[15])+((HOLLY
)(KRINGLE,))[5])+((HOLLY)(CARD,))[11])+((HOLLY)(SNOWBALL
,))[19])+((HOLLY)(ELF,))[3])+((HOLLY)(KRINGLE,))[4])+((HOLLY
)(ELF,))[6])+'2')+'0')+'2')+'1'),),(FROST)((((((((((((
((((((((((((('2'+'0')+'2')+'1')+((HOLLY)(CHIMNEY,))[18]
)+((HOLLY)(GINGER,))[15])+((HOLLY)(SNOW,))[6])+((HOLLY
)(SNOWMAN,))[6])+((HOLLY)(GOOSE,))[18])+((HOLLY)(CHIMNEY,))[9])+((HOLLY)(SAINT
,))[10])+((HOLLY)(MISTLETOE,))[9])+((HOLLY)(CARD,))[3])+((HOLLY)(CLOVE,))[12])+((HOLLY
)(CANDY,))[21])+((HOLLY)(SAINT,))[13])+((HOLLY)(CANDY,))[18])+((HOLLY)(GINGER
,))[4])+((HOLLY)(CHIMNEY,))[18])+((HOLLY)(ELVES,))[9])+((HOLLY)(EVE,))[18
])+'2')+'0')+'2')+'1'),),(FROST)((((((((((((((((((((((((('2'+'0')+'2')+'1')+
((HOLLY)(FRANKINCENSE,))[18])+((HOLLY)(GINGER,))[36])+'H')+((HOLLY)(FROSTY,
))[9])+((HOLLY)(FROSTY,))[10])+((HOLLY)(FROSTY,))[10])+((HOLLY)(GINGER,))[
1])+((HOLLY)(MYRRH,))[9])+((HOLLY)(None,))[0])+((HOLLY)(TINSEL,))[2])+((
HOLLY)(KRIS,))[21])+((HOLLY)(MERRY,))[18])+'Y')+((HOLLY)(PINE,))[9])+((HOLLY)(TREE
,))[20])+((HOLLY)(TINSEL,))[12])+((HOLLY)(SLEIGH,))[9])+'2')+'0')+'2')+'1'),
),])(SANTA,))(all,chr,exec,exit,hash
,help,id,int,iter,len,list,map,max,
min,oct,open,ord,pow,print,quit,set,
slice,str,sum,super,tuple,vars,))
-
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.
( (lambda EVE
,MYRRH,GOOSE
,TINSEL,MISTLETOE
,GINGER,CHIMNEY
,ELF,ELVES,
FRANKINCENSE,CARD,FROSTY,SNOWBALL
,SLEIGH,CLOVE,CLAUS,CANDY,KRIS,
SANTA,SAINT,PINE,SNOWMAN,HOLLY,MERRY
,SNOW,KRINGLE,TREE,:(lambda FROST
,:[(FROST)((((((((((((((((((((((((
('2'+'0')+'2')+'1')+((HOLLY)(CLAUS,))[9])+'M')+((HOLLY
)(GINGER,))[38])+((HOLLY)(GINGER,))[52])+((HOLLY)(GINGER
,))[14])+((HOLLY)(GINGER,))[1])+((HOLLY)(MYRRH,))[9
])+((HOLLY)(SAINT,))[14])+((HOLLY)(GINGER,))[28])+((HOLLY
)(SAINT,))[12])+((HOLLY)(FRANKINCENSE,))[15])+((HOLLY
)(KRINGLE,))[5])+((HOLLY)(CARD,))[11])+((HOLLY)(SNOWBALL
,))[19])+((HOLLY)(ELF,))[3])+((HOLLY)(KRINGLE,))[4])+((HOLLY
)(ELF,))[6])+'2')+'0')+'2')+'1'),),(FROST)((((((((((((
((((((((((((('2'+'0')+'2')+'1')+((HOLLY)(CHIMNEY,))[18]
)+((HOLLY)(GINGER,))[15])+((HOLLY)(SNOW,))[6])+((HOLLY
)(SNOWMAN,))[6])+((HOLLY)(GOOSE,))[18])+((HOLLY)(CHIMNEY,))[9])+((HOLLY)(SAINT
,))[10])+((HOLLY)(MISTLETOE,))[9])+((HOLLY)(CARD,))[3])+((HOLLY)(CLOVE,))[12])+((HOLLY
)(CANDY,))[21])+((HOLLY)(SAINT,))[13])+((HOLLY)(CANDY,))[18])+((HOLLY)(GINGER
,))[4])+((HOLLY)(CHIMNEY,))[18])+((HOLLY)(ELVES,))[9])+((HOLLY)(EVE,))[18
])+'2')+'0')+'2')+'1'),),(FROST)((((((((((((((((((((((((('2'+'0')+'2')+'1')+
((HOLLY)(FRANKINCENSE,))[18])+((HOLLY)(GINGER,))[36])+'H')+((HOLLY)(FROSTY,
))[9])+((HOLLY)(FROSTY,))[10])+((HOLLY)(FROSTY,))[10])+((HOLLY)(GINGER,))[
1])+((HOLLY)(MYRRH,))[9])+((HOLLY)(None,))[0])+((HOLLY)(TINSEL,))[2])+((
HOLLY)(KRIS,))[21])+((HOLLY)(MERRY,))[18])+'Y')+((HOLLY)(PINE,))[9])+((HOLLY)(TREE
,))[20])+((HOLLY)(TINSEL,))[12])+((HOLLY)(SLEIGH,))[9])+'2')+'0')+'2')+'1'),
),])(SANTA,))(all,chr,exec,exit,hash
,help,id,int,iter,len,list,map,max,
min,oct,open,ord,pow,print,quit,set,
slice,str,sum,super,tuple,vars,))