Peter Sewell

ORCID

Publication Activity (10 Years)

Years Active: 1994-2024
Publications (10 Years): 29

Top Venues

Proc. ACM Program. Lang.

ESOP

POPL

IEEE Symposium on Security and Privacy

Publications

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

Peter Sewell.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Peter Sewell