Peter Sewell
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
58
Venues
22
Active years
1994–2025
Best venue rank
A*
Where they publish
Papers
58 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | CPP | A CHERI C Memory Model for Verified Temporal Safety. | Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Wesley Filardo, Ian Stark, Peter Sewell |
| 2025 | ISCA | Precise exceptions in relaxed architectures. | Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell |
| 2025 | SOSP | Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor. | Kayvan Memarian, Ben Simner, David Kaloper-Mersinjak, Thibaut Prami, Peter Sewell |
| 2024 | ASPLOS | 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 |
| 2022 | ESOP | 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 |
| 2022 | ESOP | Relaxed virtual memory in Armv8-A. | Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell |
| 2022 | PLDI | 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 |
| 2021 | CAV | Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models. | Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell |
| 2021 | CPP | Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk). | Peter Sewell |
| 2021 | FMCAD | Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V. | Peter Sewell |
| 2020 | ESOP | ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures. | Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell |
| 2020 | SP | 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 |
| 2020 | SP | 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 |
| 2019 | ASPLOS | 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 |
| 2019 | CAV | 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 |
| 2017 | POPL | 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 |
| 2016 | OOPSLA | The missing link: explaining ELF static linking, semantically. | Stephen Kell, Dominic P. Mulligan, Peter Sewell |
| 2016 | OOPSLA | An operational semantics for C/C++11 concurrency. | Kyndylan Nienhuis, Kayvan Memarian, Peter Sewell |
| 2016 | PLDI | 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 |
| 2016 | POPL | 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 |
| 2016 | POPL | A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. | Jean Pichon-Pharabod, Peter Sewell |
| 2015 | ESOP | The Problem of Programming Language Concurrency Semantics. | Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, Peter Sewell |
| 2015 | MICRO | 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 |
| 2015 | SOSP | 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 |
| 2014 | ICFP | Lem: reusable engineering of real-world semantics. | Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, Peter Sewell |
| 2012 | CAV | 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 |
| 2012 | CONCUR | False Concurrency and Strange-but-True Machines - (Abstract). | Peter Sewell |
| 2012 | ICFP | Tales from the jungle. | Peter Sewell |
| 2012 | PLDI | Synchronising C/C++ and POWER. | Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams |
| 2012 | POPL | Clarifying and compiling C/C++ concurrency: from C++11 to POWER. | Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, Peter Sewell |
| 2011 | ITP | Lem: A Lightweight Tool for Heavyweight Semantics. | Scott Owens, Peter Bhm, Francesco Zappa Nardelli, Peter Sewell |
| 2011 | PLDI | Understanding POWER multiprocessors. | Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams |
| 2011 | POPL | Mathematizing C++ concurrency. | Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber |
| 2011 | POPL | Robin Milner 1934--2010: verification, languages, and concurrency. | Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell |
| 2011 | POPL | Relaxed-memory concurrency and verified compilation. | Jaroslav Sevck, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell |
| 2011 | TACAS | Litmus: Running Tests against Hardware. | Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell |
| 2010 | CAV | Fences in Weak Memory Models. | Jade Alglave, Luc Maranget, Susmit Sarkar, Peter Sewell |
| 2009 | POPL | 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 |
| 2009 | POPL | 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 |
| 2008 | FM | A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. | Tom Ridge, Michael Norrish, Peter Sewell |
| 2007 | ICFP | Ott: effective tool support for the working semanticist. | Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Tom Ridge, Susmit Sarkar, Rok Strnisa |
| 2007 | OOPSLA | The java module system: core design and semantic definition. | Rok Strnisa, Peter Sewell, Matthew J. Parkinson |
| 2006 | ICNP | Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL. | Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, Peter Sewell |
| 2006 | POPL | Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. | Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough |
| 2005 | ICFP | 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 |
| 2005 | POPL | Mutatis mutandis: safe and predictable dynamic software updating. | Gareth Paul Stoyle, Michael W. Hicks, Gavin M. Bierman, Peter Sewell, Iulian Neamtiu |
| 2005 | SIGCOMM | 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 |
| 2003 | ESORICS | Passive Attack Analysis for Connection-Based Anonymity Systems. | Andrei Serjantov, Peter Sewell |
| 2003 | ICFP | Dynamic rebinding for marshalling and update, with destruct-time? | Gavin M. Bierman, Michael W. Hicks, Peter Sewell, Gareth Paul Stoyle, Keith Wansbrough |
| 2003 | ICFP | Global abstraction-safe marshalling with hash types. | James J. Leifer, Gilles Peskine, Peter Sewell, Keith Wansbrough |
| 2002 | ESOP | Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. | Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov |
| 2001 | POPL | Modules, abstract types, and distributed versioning. | Peter Sewell |
| 2001 | POPL | Nomadic pict: correct communication infrastructure for mobile computation. | Asis Unyapoth, Peter Sewell |
| 2000 | LICS | Models for Name-Passing Processes: Interleaving and Causal. | Gian Luca Cattani, Peter Sewell |
| 1998 | CONCUR | From Rewrite to Bisimulation Congruences. | Peter Sewell |
| 1998 | ICALP | Global/Local Subtyping and Capability Inference for a Distributed pi-calculus. | Peter Sewell |
| 1997 | CONCUR | On Implementations and Semantics of a Concurrent Programming Language. | Peter Sewell |
| 1994 | LICS | Bisimulation is Not Finitely (First Order) Equationally Axiomatisable | Peter Sewell |