Peter Sewell

111 papers A* 31A 16B 9C 1Journal 34Unranked 18
YearRankTypeTitle / Venue / Authors
2026 J jnl
An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics.
ACM Trans. Program. Lang. Syst.
Zongyuan Liu, Angus Hammond, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod
2026 J jnl
ArchSem: Reusable Rigorous Semantics of Relaxed Architectures.
Proc. ACM Program. Lang.
Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Zongyuan Liu, Nils Lauermann, Alasdair Armstrong, Peter Sewell
2025 B conf
A CHERI C Memory Model for Verified Temporal Safety.
CPP
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Wesley Filardo, Ian Stark, Peter Sewell
2025 J jnl
Fulminate: Testing CN Separation-Logic Specifications in C.
Proc. ACM Program. Lang.
Rini Banerjee, Kayvan Memarian, Dhruv C. Makwana, Christopher Pulte, Neel Krishnaswami, Peter Sewell
2025 A* conf
Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor.
SOSP
Kayvan Memarian, Ben Simner, David Kaloper-Mersinjak, Thibaut Pérami, Peter Sewell
2025 J jnl
It Is Time to Standardize Principles and Practices for Software Memory Safety.
Commun. ACM
Robert N. M. Watson, John Baldwin, David Chisnall, Tony Chen, Jessica Clarke, Brooks Davis, Nathaniel Wesley Filardo, Brett F. Gutstein, Graeme Jenkinson, Ben Laurie, Alfredo Mazzinghi, Simon W. Moore, Peter G. Neumann, Hamed Okhravi, Alex Richardson, Alex Rebert, Peter Sewell, Laurence Tratt, Murali Vijayaraghavan, Hugo Vincent, Konrad Witaszczyk
2025 J jnl
Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture.
Proc. ACM Program. Lang.
Angus Hammond, Ricardo Almeida, Thomas Bauereiss, Brian Campbell, Ian Stark, Peter Sewell
2025 A* conf
Precise exceptions in relaxed architectures.
ISCA
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell
2024 J jnl
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic.
Proc. ACM Program. Lang.
Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod
2024 J jnl
CHERI: Hardware-Enabled C/C++ Memory Protection at Scale.
IEEE Secur. Priv.
Robert N. M. Watson, David Chisnall, Jessica Clarke, Brooks Davis, Nathaniel Wesley Filardo, Ben Laurie, Simon W. Moore, Peter G. Neumann, Alexander Richardson, Peter Sewell, Konrad Witaszczyk, Jonathan Woodruff
2024 — conf
Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance.
ASPLOS (1)
Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alexander Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, Peter Sewell
2024 J jnl
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version).
Formal Methods Syst. Des.
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
2024 J jnl
Relaxed exception semantics for Arm-A (extended version).
CoRR
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell
2023 J jnl
CN: Verifying Systems C Code with Separation-Logic Refinement Types.
Proc. ACM Program. Lang.
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami
2023 J jnl
The Arm Morello Evaluation Platform - Validating CHERI-Based Security in a High-Performance System.
IEEE Micro
Richard Grisenthwaite, Graeme Barnes, Robert N. M. Watson, Simon W. Moore, Peter Sewell, Jonathan Woodruff
2022 A* conf
Islaris: verification of machine code against authoritative ISA semantics.
PLDI
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell
2022 J jnl
Relaxed virtual memory in Armv8-A (extended version).
CoRR
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell
2022 A conf
Relaxed virtual memory in Armv8-A.
ESOP
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell
2022 J jnl
VIP: verifying real-world C idioms with integer-pointer casts.
Proc. ACM Program. Lang.
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
2022 A conf
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture.
ESOP
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell
2021 B conf
Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V.
FMCAD
Peter Sewell
2021 — conf
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models.
CAV (1)
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
2021 B conf
Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk).
CPP
Peter Sewell
2020 A conf
ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures.
ESOP
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell
2020 A* conf
Cornucopia: Temporal Safety for CHERI Heaps.
SP
Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Sam Ainsworth, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Tomasz Napierala, Alexander Richardson, John Baldwin, David Chisnall, Jessica Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo Mazzinghi, Robert M. Norton, Michael Roe, Peter Sewell, Stacey D. Son, Timothy M. Jones, Simon W. Moore, Peter G. Neumann, Robert N. M. Watson
2020 A* conf
Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process.
SP
Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony C. J. Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, Peter Sewell
2019 — conf
Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C.
CAV (1)
Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean Pichon-Pharabod, Peter Sewell
2019 A* conf
CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment.
ASPLOS
Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, Jessica Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey D. Son, Jonathan Woodruff
2019 J jnl
Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API.
J. ACM
Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, Keith Wansbrough
2019 J jnl
Exploring C semantics and pointer provenance.
Proc. ACM Program. Lang.
Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, Peter Sewell
2019 J jnl
ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS.
Proc. ACM Program. Lang.
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, Peter Sewell
2019 J jnl
Through computer architecture, darkly.
Commun. ACM
A. Theodore Markettos, Robert N. M. Watson, Simon W. Moore, Peter Sewell, Peter G. Neumann
2018 J jnl
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8.
Proc. ACM Program. Lang.
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell
2017 A* conf
Mixed-size concurrency: ARM, POWER, C/C++11, and SC.
POPL
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, Peter Sewell
2016 A* conf
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions.
POPL
Jean Pichon-Pharabod, Peter Sewell
2016 A conf
An operational semantics for C/C++11 concurrency.
OOPSLA
Kyndylan Nienhuis, Kayvan Memarian, Peter Sewell
2016 A* conf
Into the depths of C: elaborating the de facto standards.
PLDI
Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson, Peter Sewell
2016 A* conf
Modelling the ARMv8 architecture, operationally: concurrency and ISA.
POPL
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell
2016 A conf
The missing link: explaining ELF static linking, semantically.
OOPSLA
Stephen Kell, Dominic P. Mulligan, Peter Sewell
2015 A* conf
An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors.
MICRO
Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, Peter Sewell
2015 A* conf
Not-Quite-So-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation.
USENIX Security Symposium
David Kaloper-Mersinjak, Hannes Mehnert, Anil Madhavapeddy, Peter Sewell
2015 A* conf
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems.
SOSP
Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, Peter Sewell
2015 A conf
The Problem of Programming Language Concurrency Semantics.
ESOP
Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, Peter Sewell
2014 A conf
Lem: reusable engineering of real-world semantics.
ICFP
Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, Peter Sewell
2014 J jnl
POPL 2014 program chair's report.
ACM SIGPLAN Notices
Peter Sewell
2014 — ed.
Proceedings of the 3rd ACM SIGPLAN Program Protection and Reverse Engineering Workshop 2014, PPREW 2014, January 25, 2014, San Diego, CA, USA
PPREW@POPL
Suresh Jagannathan, Peter Sewell
2014 A* ed.
The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014
POPL
Suresh Jagannathan, Peter Sewell
2013 J jnl
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.
J. ACM
Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
2013 J jnl
Principles of POPL.
ACM SIGPLAN Notices
Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell, Philip Wadler
2012 A* conf
An Axiomatic Memory Model for POWER Multiprocessors.
CAV
Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, Derek Williams
2012 A* conf
Clarifying and compiling C/C++ concurrency: from C++11 to POWER.
POPL
Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, Peter Sewell
2012 B conf
False Concurrency and Strange-but-True Machines - (Abstract).
CONCUR
Peter Sewell
2012 J jnl
Fences in weak memory models (extended version).
Formal Methods Syst. Des.
Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell
2012 A* conf
Synchronising C/C++ and POWER.
PLDI
Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams
2012 A conf
Tales from the jungle.
ICFP
Peter Sewell
2011 B conf
Lem: A Lightweight Tool for Heavyweight Semantics.
ITP
Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell
2011 A conf
Litmus: Running Tests against Hardware.
TACAS
Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell
2011 A* conf
Mathematizing C++ concurrency.
POPL
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber
2011 J jnl
Multi-Core Memory Models and Concurrency Theory (Dagstuhl Seminar 11011).
Dagstuhl Reports
Hans-Juergen Boehm, Ursula Goltz, Holger Hermanns, Peter Sewell
2011 A* conf
Relaxed-memory concurrency and verified compilation.
POPL
Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell
2011 A* conf
Robin Milner 1934--2010: verification, languages, and concurrency.
POPL
Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell
2011 A* conf
Understanding POWER multiprocessors.
PLDI
Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams
2010 A* conf
Fences in Weak Memory Models.
CAV
Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell
2010 C conf
Memory, an elusive abstraction.
ISMM
Peter Sewell
2010 J jnl
Nomadic pict: Programming languages, communication infrastructure overlays, and semantics for mobile computation.
ACM Trans. Program. Lang. Syst.
Peter Sewell, Pawel T. Wojciechowski, Asis Unyapoth
2010 J jnl
Ott: Effective tool support for the working semanticist.
J. Funct. Program.
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strnisa
2010 J jnl
x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors.
Commun. ACM
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen
2009 — conf
A Better x86 Memory Model: x86-TSO.
TPHOLs
Scott Owens, Susmit Sarkar, Peter Sewell
2009 — conf
The semantics of power and ARM multiprocessor machine code.
DAMP
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli
2009 A* conf
The semantics of x86-CC multiprocessor machine code.
POPL
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave
2008 B conf
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service.
FM
Tom Ridge, Michael Norrish, Peter Sewell
2008 J jnl
Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction.
J. Funct. Program.
Peter Sewell, Gareth Paul Stoyle, Michael Hicks, Gavin M. Bierman, Keith Wansbrough
2007 J jnl
Acute: High-level programming language design for distributed computation.
J. Funct. Program.
Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis
2007 A conf
Ott: effective tool support for the working semanticist.
ICFP
Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strnisa
2007 A conf
The java module system: core design and semantic definition.
OOPSLA
Rok Strnisa, Peter Sewell, Matthew J. Parkinson
2006 A* conf
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations.
POPL
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
2006 B conf
Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL.
ICNP
Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, Peter Sewell
2006 — conf
Type-safe distributed programming for OCaml.
ML
John Billings, Peter Sewell, Mark R. Shinwell, Rok Strnisa
2005 A conf
Acute: high-level programming language design for distributed computation.
ICFP
Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis
2005 — conf
It Is Time to Mechanize Programming Language Metatheory.
VSTTE
Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic
2005 — conf
Mechanized Metatheory for the Masses: The PoplMark Challenge.
TPHOLs
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic
2005 A* conf
Mutatis mutandis: safe and predictable dynamic software updating.
POPL
Gareth Paul Stoyle, Michael W. Hicks, Gavin M. Bierman, Peter Sewell, Iulian Neamtiu
2005 J jnl
Passive-attack analysis for connection-based anonymity systems.
Int. J. Inf. Sec.
Andrei Serjantov, Peter Sewell
2005 — conf
Process Calculi: The End of the Beginning?: (From Thought Experiments to Experimental Semantics).
APC 25
Peter Sewell
2005 A* conf
Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets.
SIGCOMM
Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
2004 — conf
Cassandra: Distributed Access Control Policies with Tunable Expressiveness.
POLICY
Moritz Y. Becker, Peter Sewell
2004 — conf
Cassandra: Flexible Trust Management, Applied to Electronic Health Records.
CSFW
Moritz Y. Becker, Peter Sewell
2004 J jnl
Models for name-passing processes: interleaving and causal.
Inf. Comput.
Gian Luca Cattani, Peter Sewell
2003 A conf
Dynamic rebinding for marshalling and update, with destruct-time?
ICFP
Gavin M. Bierman, Michael W. Hicks, Peter Sewell, Gareth Paul Stoyle, Keith Wansbrough
2003 A conf
Global abstraction-safe marshalling with hash types.
ICFP
James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough
2003 A conf
Passive Attack Analysis for Connection-Based Anonymity Systems.
ESORICS
Andrei Serjantov, Peter Sewell
2003 J jnl
Secure Composition of Untrusted Code: Box pi, Wrappers, and Causality.
J. Comput. Secur.
Peter Sewell, Jan Vitek
2002 J jnl
From rewrite rules to bisimulation congruences.
Theor. Comput. Sci.
Peter Sewell
2002 — conf
Rigour is good for you
ACM SIGOPS European Workshop
Michael Norrish, Peter Sewell, Keith Wansbrough
2002 A conf
Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures.
ESOP
Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov
2001 A* conf
Modules, abstract types, and distributed versioning.
POPL
Peter Sewell
2001 A* conf
Nomadic pict: correct communication infrastructure for mobile computation.
POPL
Asis Unyapoth, Peter Sewell
2001 — conf
The UDP Calculus: Rigorous Semantics for Real Networking.
TACS
Andrei Serjantov, Peter Sewell, Keith Wansbrough
2000 — ed.
4th International Workshop on High-Level Concurrent Languages, HLCL 2000, Satellite to PLI 2000, Montreal, Canada, September 20, 2000
HLCL
John H. Reppy, Peter Sewell
2000 A* conf
Models for Name-Passing Processes: Interleaving and Causal.
LICS
Gian Luca Cattani, Peter Sewell
2000 J jnl
Nomadic Pict: language and infrastructure design for mobile agents.
IEEE Concurr.
Pawel T. Wojciechowski, Peter Sewell
2000 — conf
Preface.
HLCL
Peter Sewell
2000 — conf
Secure Composition of Untrusted Code: Wrappers and Causality Types.
CSFW
Peter Sewell, Jan Vitek
1999 — conf
Nomadic Pict: Language and Infrastructure Design for Mobile Agents.
ASA/MA
Pawel T. Wojciechowski, Peter Sewell
1999 — conf
Secure Composition of Insecure Components.
CSFW
Peter Sewell, Jan Vitek
1998 B conf
From Rewrite to Bisimulation Congruences.
CONCUR
Peter Sewell
1998 A* conf
Global/Local Subtyping and Capability Inference for a Distributed pi-calculus.
ICALP
Peter Sewell
1998 — conf
Location-Independent Communication for Mobile Agents: A Two-Level Architecture.
ICCL Workshop: Internet Programming Languages
Peter Sewell, Pawel T. Wojciechowski, Benjamin C. Pierce
1997 J jnl
Nonaxiomatisability of Equivalences over Finite State Processes.
Ann. Pure Appl. Log.
Peter Sewell
1997 B conf
On Implementations and Semantics of a Concurrent Programming Language.
CONCUR
Peter Sewell
1994 A* conf
Bisimulation is Not Finitely (First Order) Equationally Axiomatisable
LICS
Peter Sewell