-
Isla: Integrating full-scale ISA semantics and axiomatic
concurrency models (extended version).
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte,
and Peter Sewell.
Formal Methods in System Design, May 2023.
[ bib |
doi |
pdf |
http |
abstract ]
-
Multicore Semantics: Making Sense of Relaxed Memory (MPhil
slides), Peter Sewell, Christopher Pulte, Shaked Flur, Mark
Batty, Luc Maranget, and Alasdair Armstrong, October 2022.
[ bib |
.pdf ]
-
Islaris: Verification of Machine Code Against Authoritative
ISA Semantics.
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell,
Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell.
In PLDI 2022.
[ bib |
doi |
project page |
pdf |
abstract ]
-
Verified Security for the Morello Capability-enhanced
Prototype Arm Architecture.
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong,
Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, and Peter
Sewell.
In ESOP 2022.
[ bib |
doi |
project page |
pdf |
http |
abstract ]
-
Isla: Integrating full-scale ISA semantics and axiomatic
concurrency models.
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte,
and Peter Sewell.
In CAV 2021.
[ bib |
doi |
pdf |
http |
abstract ]
-
ISA Semantics for ARMv8-A, RISC-V, and
CHERI-MIPS.
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid,
Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon
French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and
Peter Sewell.
In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 71.
[ bib |
doi |
supplementary material |
project page |
pdf |
abstract ]
-
Formalisation of MiniSail in the Isabelle Theorem
Prover.
Alasdair Armstrong, Neel Krishnaswami, Peter Sewell, and Mark
Wassell.
In Automated Reasoning Workshop (ARW) 2018, Two-page abstract.
[ bib |
project page |
pdf |
abstract ]
-
Detailed Models of Instruction Set Architectures: From
Pseudocode to Formal Semantics.
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Shaked Flur,
Kathryn E. Gray, Prashanth Mundkur, Robert M. Norton, Christopher Pulte,
Alastair Reid, Peter Sewell, Ian Stark, and Mark Wassell.
In Automated Reasoning Workshop (ARW) 2018, Two-page abstract.
[ bib |
project page |
pdf |
abstract ]
-
Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and
Operational Models for ARMv8.
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit
Sarkar, and Peter Sewell.
In POPL 2018.
[ bib |
doi |
project page |
errata |
pdf |
abstract ]
-
Mixed-size Concurrency: ARM, POWER, C/C++11, and
SC.
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc
Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell.
In POPL 2017.
[ bib |
doi |
project page |
pdf |
abstract ]
-
Modelling the ARMv8 architecture, operationally: concurrency
and ISA.
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali
Sezgin, Luc Maranget, Will Deacon, and Peter Sewell.
In POPL 2016.
[ bib |
doi |
project page |
pdf |
abstract ]
-
An integrated concurrency and core-ISA architectural envelope
definition, and test oracle, for IBM POWER multiprocessors
.
Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher
Pulte, Susmit Sarkar, and Peter Sewell.
In MICRO 2015.
[ bib |
doi |
pdf |
abstract ]