• 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 ]