Peter Sewell

According to our database, Peter Sewell authored at least 93 papers between 1994 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic.

Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod

Proc. ACM Program. Lang., January, 2024

Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance.

Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alexander Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, Peter Sewell

Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2024

2023

CN: Verifying Systems C Code with Separation-Logic Refinement Types.

Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami

Proc. ACM Program. Lang., January, 2023

The Arm Morello Evaluation Platform - Validating CHERI-Based Security in a High-Performance System.

Richard Grisenthwaite, Graeme Barnes, Robert N. M. Watson, Simon W. Moore, Peter Sewell, Jonathan Woodruff

IEEE Micro, 2023

2022

VIP: verifying real-world C idioms with integer-pointer casts.

Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell

Proc. ACM Program. Lang., 2022

Relaxed virtual memory in Armv8-A (extended version).

Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell

CoRR, 2022

Islaris: verification of machine code against authoritative ISA semantics.

Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Relaxed virtual memory in Armv8-A.

Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell

Proceedings of the Programming Languages and Systems, 2022

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, Peter Sewell

Proceedings of the Programming Languages and Systems, 2022

2021

Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V.

Peter Sewell

Proceedings of the Formal Methods in Computer Aided Design, 2021

Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk).

Peter Sewell

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models.

Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process.

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

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Cornucopia: Temporal Safety for CHERI Heaps.

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

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures.

Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell

Proceedings of the Programming Languages and Systems, 2020

2019

Exploring C semantics and pointer provenance.

Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, Peter Sewell

Proc. ACM Program. Lang., 2019

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, Peter Sewell

Proc. ACM Program. Lang., 2019

Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API.

Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, Keith Wansbrough

J. ACM, 2019

Through computer architecture, darkly.

A. Theodore Markettos, Robert N. M. Watson, Simon W. Moore, Peter Sewell, Peter G. Neumann

Commun. ACM, 2019

Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C.

Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean Pichon-Pharabod, Peter Sewell

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment.

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

Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, 2019

2018

Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8.

Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell

Proc. ACM Program. Lang., 2018

2017

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, Peter Sewell

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions.

Jean Pichon-Pharabod, Peter Sewell

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Modelling the ARMv8 architecture, operationally: concurrency and ISA.

Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Into the depths of C: elaborating the de facto standards.

Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson, Peter Sewell

Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

An operational semantics for C/C++11 concurrency.

Kyndylan Nienhuis, Kayvan Memarian, Peter Sewell

Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

The missing link: explaining ELF static linking, semantically.

Stephen Kell, Dominic P. Mulligan, Peter Sewell

Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016

2015

Not-Quite-So-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation.

David Kaloper-Mersinjak, Hannes Mehnert, Anil Madhavapeddy, Peter Sewell

Proceedings of the 24th USENIX Security Symposium, 2015

SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems.

Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, Peter Sewell

Proceedings of the 25th Symposium on Operating Systems Principles, 2015

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, Peter Sewell

Proceedings of the 48th International Symposium on Microarchitecture, 2015

The Problem of Programming Language Concurrency Semantics.

Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, Peter Sewell

Proceedings of the Programming Languages and Systems, 2015

2014

POPL 2014 program chair's report.

Peter Sewell

ACM SIGPLAN Notices, 2014

Lem: reusable engineering of real-world semantics.

Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, Peter Sewell

Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, 2014

2013

Principles of POPL.

Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell, Philip Wadler

ACM SIGPLAN Notices, 2013

CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency.

Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell

J. ACM, 2013

2012

Fences in weak memory models (extended version).

Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell

Formal Methods Syst. Des., 2012

Clarifying and compiling C/C++ concurrency: from C++11 to POWER.

Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, Peter Sewell

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Synchronising C/C++ and POWER.

Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams

Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Tales from the jungle.

Peter Sewell

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

False Concurrency and Strange-but-True Machines - (Abstract).

Peter Sewell

Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012

An Axiomatic Memory Model for POWER Multiprocessors.

Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, Derek Williams

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Multi-Core Memory Models and Concurrency Theory (Dagstuhl Seminar 11011).

Hans-Juergen Boehm, Ursula Goltz, Holger Hermanns, Peter Sewell

Dagstuhl Reports, 2011

Litmus: Running Tests against Hardware.

Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Relaxed-memory concurrency and verified compilation.

Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Robin Milner 1934--2010: verification, languages, and concurrency.

Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Mathematizing C++ concurrency.

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Understanding POWER multiprocessors.

Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams

Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

Lem: A Lightweight Tool for Heavyweight Semantics.

Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

2010

Nomadic pict: Programming languages, communication infrastructure overlays, and semantics for mobile computation.

Peter Sewell, Pawel T. Wojciechowski, Asis Unyapoth

ACM Trans. Program. Lang. Syst., 2010

Ott: Effective tool support for the working semanticist.

Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, Rok Strnisa

J. Funct. Program., 2010

x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors.

Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen

Commun. ACM, 2010

Memory, an elusive abstraction.

Peter Sewell

Proceedings of the 9th International Symposium on Memory Management, 2010

Fences in Weak Memory Models.

Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

A Better x86 Memory Model: x86-TSO.

Scott Owens, Susmit Sarkar, Peter Sewell

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

The semantics of x86-CC multiprocessor machine code.

Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

The semantics of power and ARM multiprocessor machine code.

Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli

Proceedings of the POPL 2009 Workshop on Declarative Aspects of Multicore Programming, 2009

2008

Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction.

Peter Sewell, Gareth Paul Stoyle, Michael Hicks, Gavin M. Bierman, Keith Wansbrough

J. Funct. Program., 2008

A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service.

Tom Ridge, Michael Norrish, Peter Sewell

Proceedings of the FM 2008: Formal Methods, 2008

2007

<i>Mutatis Mutandis</i>: Safe and predictable dynamic software updating.

Gareth Paul Stoyle, Michael W. Hicks, Gavin M. Bierman, Peter Sewell, Iulian Neamtiu

ACM Trans. Program. Lang. Syst., 2007

Acute: High-level programming language design for distributed computation.

Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis

J. Funct. Program., 2007

The java module system: core design and semantic definition.

Rok Strnisa, Peter Sewell, Matthew J. Parkinson

Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

2006

Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations.

Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

Type-safe distributed programming for OCaml.

John Billings, Peter Sewell, Mark R. Shinwell, Rok Strnisa

Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006, 2006

Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL.

Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, Peter Sewell

Proceedings of the 14th IEEE International Conference on Network Protocols, 2006

2005

Passive-attack analysis for connection-based anonymity systems.

Andrei Serjantov, Peter Sewell

Int. J. Inf. Sec., 2005

Process Calculi: The End of the Beginning?: (From Thought Experiments to Experimental Semantics).

Peter Sewell

Proceedings of the Workshop "Essays on Algebraic Process Calculi", 2005

It Is Time to Mechanize Programming Language Metatheory.

Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic

Proceedings of the Verified Software: Theories, 2005

Mechanized Metatheory for the Masses: The PoplMark Challenge.

Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets.

Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough

Proceedings of the ACM SIGCOMM 2005 Conference on Applications, 2005

Mutatis mutandis: safe and predictable dynamic software updating.

Gareth Paul Stoyle, Michael W. Hicks, Gavin M. Bierman, Peter Sewell, Iulian Neamtiu

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

2004

Models for name-passing processes: interleaving and causal.

Gian Luca Cattani, Peter Sewell

Inf. Comput., 2004

Cassandra: Distributed Access Control Policies with Tunable Expressiveness.

Moritz Y. Becker, Peter Sewell

Proceedings of the 5th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY 2004), 2004

Cassandra: Flexible Trust Management, Applied to Electronic Health Records.

Moritz Y. Becker, Peter Sewell

Proceedings of the 17th IEEE Computer Security Foundations Workshop, 2004

2003

Secure Composition of Untrusted Code: Box pi, Wrappers, and Causality.

Peter Sewell, Jan Vitek

J. Comput. Secur., 2003

Global abstraction-safe marshalling with hash types.

James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough

Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

Dynamic rebinding for marshalling and update, with destruct-time?

Gavin M. Bierman, Michael W. Hicks, Peter Sewell, Gareth Paul Stoyle, Keith Wansbrough

Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

2002

From rewrite rules to bisimulation congruences.

Peter Sewell

Theor. Comput. Sci., 2002

Rigour is good for you <i>and</i> feasible: reflections on formal treatments of C and UDP sockets.

Michael Norrish, Peter Sewell, Keith Wansbrough

Proceedings of the 10th ACM SIGOPS European Workshop, Saint-Emilion, France, July 1, 2002, 2002

Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures.

Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov

Proceedings of the Programming Languages and Systems, 2002

2001

The UDP Calculus: Rigorous Semantics for Real Networking.

Andrei Serjantov, Peter Sewell, Keith Wansbrough

Proceedings of the Theoretical Aspects of Computer Software, 4th International Symposium, 2001

Nomadic pict: correct communication infrastructure for mobile computation.

Asis Unyapoth, Peter Sewell

Proceedings of the Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001

Modules, abstract types, and distributed versioning.

Peter Sewell

Proceedings of the Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001

2000

Nomadic Pict: language and infrastructure design for mobile agents.

Pawel T. Wojciechowski, Peter Sewell

IEEE Concurr., 2000

Preface.

Peter Sewell

Proceedings of the 4th International Workshop on High-Level Concurrent Languages, 2000

Secure Composition of Untrusted Code: Wrappers and Causality Types.

Peter Sewell, Jan Vitek

Proceedings of the 13th IEEE Computer Security Foundations Workshop, 2000

1999

Secure Composition of Insecure Components.

Peter Sewell, Jan Vitek

Proceedings of the 12th IEEE Computer Security Foundations Workshop, 1999

1998

Location-Independent Communication for Mobile Agents: A Two-Level Architecture.

Peter Sewell, Pawel T. Wojciechowski, Benjamin C. Pierce

Proceedings of the Internet Programming Languages, 1998

Global/Local Subtyping and Capability Inference for a Distributed pi-calculus.

Peter Sewell

Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

From Rewrite to Bisimulation Congruences.

Peter Sewell

Proceedings of the CONCUR '98: Concurrency Theory, 1998

1997

Nonaxiomatisability of Equivalences over Finite State Processes.

Peter Sewell

Ann. Pure Appl. Log., 1997

On Implementations and Semantics of a Concurrent Programming Language.

Peter Sewell

Proceedings of the CONCUR '97: Concurrency Theory, 1997

1994

Bisimulation is Not Finitely (First Order) Equationally Axiomatisable

Peter Sewell

Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994