default search action
Peter Sewell
Person information
- affiliation: University of Cambridge, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j27]Alasdair Armstrong
, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell:
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version). Formal Methods Syst. Des. 63(1): 110-133 (2024) - [j26]Robert N. M. Watson
CHERI: Hardware-Enabled C/C++ Memory Protection at Scale. IEEE Secur. Priv. 22(4): 50-61 (2024) - [j25]Angus Hammond
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. Proc. ACM Program. Lang. 8(POPL): 604-637 (2024) - [c71]Vadim Zaliva
Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance. ASPLOS (1) 2024: 181-196 - 2023
- [j24]Richard Grisenthwaite
The Arm Morello Evaluation Platform - Validating CHERI-Based Security in a High-Performance System. IEEE Micro 43(3): 50-57 (2023) - [j23]Christopher Pulte
CN: Verifying Systems C Code with Separation-Logic Refinement Types. Proc. ACM Program. Lang. 7(POPL): 1-32 (2023) - 2022
- [j22]Rodolphe Lepigre
VIP: verifying real-world C idioms with integer-pointer casts. Proc. ACM Program. Lang. 6(POPL): 1-32 (2022) - [c70]Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte
Relaxed virtual memory in Armv8-A. ESOP 2022: 143-173 - [c69]Thomas Bauereiss
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. ESOP 2022: 174-203 - [c68]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: 825-840 - [i2]Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell:
Relaxed virtual memory in Armv8-A (extended version). CoRR abs/2203.00642 (2022) - 2021
- [c67]Alasdair Armstrong, Brian Campbell
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models. CAV (1) 2021: 303-316 - [c66]Peter Sewell:
Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk). CPP 2021: 4 - [c65]Peter Sewell:
Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V. FMCAD 2021: 12 - 2020
- [c64]Ben Simner, Shaked Flur, Christopher Pulte
ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures. ESOP 2020: 626-655 - [c63]Nathaniel Wesley Filardo
Cornucopia: Temporal Safety for CHERI Heaps. SP 2020: 608-625 - [c62]Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony C. J. Fox, Michael Roe, Brian Campbell
Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. SP 2020: 1003-1020
2010 – 2019
- 2019
- [j21]A. Theodore Markettos, Robert N. M. Watson, Simon W. Moore, Peter Sewell, Peter G. Neumann:
Through computer architecture, darkly. Commun. ACM 62(6): 25-27 (2019) - [j20]Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish
Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API. J. ACM 66(1): 1:1-1:77 (2019) - [j19]Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson
Exploring C semantics and pointer provenance. Proc. ACM Program. Lang. 3(POPL): 67:1-67:32 (2019) - [j18]Alasdair Armstrong, Thomas Bauereiss, Brian Campbell
ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. Proc. ACM Program. Lang. 3(POPL): 71:1-71:31 (2019) - [c61]Brooks Davis, Robert N. M. Watson, Alexander Richardson
CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment. ASPLOS 2019: 379-393 - [c60]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: 387-397 - 2018
- [j17]Christopher Pulte
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang. 2(POPL): 19:1-19:29 (2018) - 2017
- [c59]Shaked Flur, Susmit Sarkar
Mixed-size concurrency: ARM, POWER, C/C++11, and SC. POPL 2017: 429-442 - 2016
- [c58]Kyndylan Nienhuis, Kayvan Memarian, Peter Sewell
An operational semantics for C/C++11 concurrency. OOPSLA 2016: 111-128 - [c57]Stephen Kell, Dominic P. Mulligan
The missing link: explaining ELF static linking, semantically. OOPSLA 2016: 607-623 - [c56]Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall
Into the depths of C: elaborating the de facto standards. PLDI 2016: 1-15 - [c55]Shaked Flur, Kathryn E. Gray, Christopher Pulte
Modelling the ARMv8 architecture, operationally: concurrency and ISA. POPL 2016: 608-621 - [c54]Jean Pichon-Pharabod, Peter Sewell
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. POPL 2016: 622-633 - 2015
- [c53]Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, Peter Sewell
The Problem of Programming Language Concurrency Semantics. ESOP 2015: 283-307 - [c52]Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan
An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. MICRO 2015: 635-646 - [c51]Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. SOSP 2015: 38-53 - [c50]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: 223-238 - 2014
- [j16]Peter Sewell
POPL 2014 program chair's report. ACM SIGPLAN Notices 49(4S): 10-26 (2014) - [c49]Dominic P. Mulligan
Lem: reusable engineering of real-world semantics. ICFP 2014: 175-188 - [e3]Suresh Jagannathan, Peter Sewell:
The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014. ACM 2014, ISBN 978-1-4503-2544-8 [contents] - [e2]Suresh Jagannathan, Peter Sewell:
Proceedings of the 3rd ACM SIGPLAN Program Protection and Reverse Engineering Workshop 2014, PPREW 2014, January 25, 2014, San Diego, CA, USA. ACM 2014, ISBN 978-1-4503-2649-0 [contents] - 2013
- [j15]Jaroslav Sevcík, Viktor Vafeiadis
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM 60(3): 22:1-22:50 (2013) - [j14]Derek Dreyer, John Field, Roberto Giacobazzi, Michael Hicks, Suresh Jagannathan, Mooly Sagiv, Peter Sewell
Principles of POPL. ACM SIGPLAN Notices 48(4S): 12-16 (2013) - 2012
- [j13]Jade Alglave, Luc Maranget, Susmit Sarkar
Fences in weak memory models (extended version). Formal Methods Syst. Des. 40(2): 170-205 (2012) - [c48]Sela Mador-Haim, Luc Maranget, Susmit Sarkar
An Axiomatic Memory Model for POWER Multiprocessors. CAV 2012: 495-512 - [c47]Peter Sewell
False Concurrency and Strange-but-True Machines - (Abstract). CONCUR 2012: 37-38 - [c46]Peter Sewell
Tales from the jungle. ICFP 2012: 271-272 - [c45]Susmit Sarkar
Synchronising C/C++ and POWER. PLDI 2012: 311-322 - [c44]Mark Batty, Kayvan Memarian, Scott Owens
Clarifying and compiling C/C++ concurrency: from C++11 to POWER. POPL 2012: 509-520 - 2011
- [c43]Scott Owens
Lem: A Lightweight Tool for Heavyweight Semantics. ITP 2011: 363-369 - [c42]Susmit Sarkar
Understanding POWER multiprocessors. PLDI 2011: 175-186 - [c41]Jaroslav Sevcík, Viktor Vafeiadis
Relaxed-memory concurrency and verified compilation. POPL 2011: 43-54 - [c40]Mark Batty, Scott Owens
Mathematizing C++ concurrency. POPL 2011: 55-66 - [c39]Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell
Robin Milner 1934--2010: verification, languages, and concurrency. POPL 2011: 473-474 - [c38]Jade Alglave, Luc Maranget, Susmit Sarkar
Litmus: Running Tests against Hardware. TACAS 2011: 41-44 - [i1]Hans-Juergen Boehm, Ursula Goltz, Holger Hermanns
Multi-Core Memory Models and Concurrency Theory (Dagstuhl Seminar 11011). Dagstuhl Reports 1(1): 1-26 (2011) - 2010
- [j12]Peter Sewell
x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Commun. ACM 53(7): 89-97 (2010) - [j11]Peter Sewell
Ott: Effective tool support for the working semanticist. J. Funct. Program. 20(1): 71-122 (2010) - [j10]Peter Sewell
Nomadic pict: Programming languages, communication infrastructure overlays, and semantics for mobile computation. ACM Trans. Program. Lang. Syst. 32(4): 12:1-12:63 (2010) - [c37]Jade Alglave, Luc Maranget, Susmit Sarkar
Fences in Weak Memory Models. CAV 2010: 258-272 - [c36]Peter Sewell
Memory, an elusive abstraction. ISMM 2010: 51-52
2000 – 2009
- 2009
- [c35]Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar
The semantics of power and ARM multiprocessor machine code. DAMP 2009: 13-24 - [c34]Susmit Sarkar
The semantics of x86-CC multiprocessor machine code. POPL 2009: 379-391 - [c33]Scott Owens
A Better x86 Memory Model: x86-TSO. TPHOLs 2009: 391-407 - 2008
- [j9]Peter Sewell
Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction. J. Funct. Program. 18(4): 437-502 (2008) - [c32]Tom Ridge, Michael Norrish
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. FM 2008: 294-309 - 2007
- [j8]Peter Sewell
Acute: High-level programming language design for distributed computation. J. Funct. Program. 17(4-5): 547-612 (2007) - [j7]Gareth Paul Stoyle, Michael W. Hicks, Gavin M. Bierman, Peter Sewell
Mutatis Mutandis: Safe and predictable dynamic software updating. ACM Trans. Program. Lang. Syst. 29(4): 22 (2007) - [c31]Peter Sewell
Ott: effective tool support for the working semanticist. ICFP 2007: 1-12 - [c30]Rok Strnisa, Peter Sewell
The java module system: core design and semantic definition. OOPSLA 2007: 499-514 - 2006
- [c29]Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, Peter Sewell
Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL. ICNP 2006: 117-126 - [c28]John Billings, Peter Sewell
Type-safe distributed programming for OCaml. ML 2006: 20-31 - [c27]Steve Bishop, Matthew Fairbairn, Michael Norrish
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. POPL 2006: 55-66 - 2005
- [j6]Andrei Serjantov, Peter Sewell
Passive-attack analysis for connection-based anonymity systems. Int. J. Inf. Sec. 4(3): 172-180 (2005) - [c26]Peter Sewell
Acute: high-level programming language design for distributed computation. ICFP 2005: 15-26 - [c25]Gareth Paul Stoyle, Michael W. Hicks
Mutatis mutandis: safe and predictable dynamic software updating. POPL 2005: 183-194 - [c24]Steve Bishop, Matthew Fairbairn, Michael Norrish
Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets. SIGCOMM 2005: 265-276 - [c23]Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell
Mechanized Metatheory for the Masses: The PoplMark Challenge. TPHOLs 2005: 50-65 - [c22]Benjamin C. Pierce, Peter Sewell
It Is Time to Mechanize Programming Language Metatheory. VSTTE 2005: 26-30 - [c21]Peter Sewell
Process Calculi: The End of the Beginning?: (From Thought Experiments to Experimental Semantics). APC 25 2005: 317-321 - 2004
- [j5]Gian Luca Cattani, Peter Sewell
Models for name-passing processes: interleaving and causal. Inf. Comput. 190(2): 136-178 (2004) - [c20]Moritz Y. Becker, Peter Sewell
Cassandra: Flexible Trust Management, Applied to Electronic Health Records. CSFW 2004: 139-154 - [c19]Moritz Y. Becker, Peter Sewell
Cassandra: Distributed Access Control Policies with Tunable Expressiveness. POLICY 2004: 159-168 - 2003
- [j4]Peter Sewell, Jan Vitek:
Secure Composition of Untrusted Code: Box pi, Wrappers, and Causality. J. Comput. Secur. 11(2): 135-188 (2003) - [c18]Andrei Serjantov, Peter Sewell:
Passive Attack Analysis for Connection-Based Anonymity Systems. ESORICS 2003: 116-131 - [c17]James J. Leifer, Gilles Peskine, Peter Sewell
Global abstraction-safe marshalling with hash types. ICFP 2003: 87-98 - [c16]Gavin M. Bierman, Michael W. Hicks
Dynamic rebinding for marshalling and update, with destruct-time? ICFP 2003: 99-110 - 2002
- [j3]Peter Sewell
From rewrite rules to bisimulation congruences. Theor. Comput. Sci. 274(1-2): 183-230 (2002) - [c15]Keith Wansbrough, Michael Norrish, Peter Sewell
Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. ESOP 2002: 278-294 - [c14]Michael Norrish, Peter Sewell
Rigour is good for you and feasible: reflections on formal treatments of C and UDP sockets. ACM SIGOPS European Workshop 2002: 49-53 - 2001
- [c13]Asis Unyapoth, Peter Sewell
Nomadic pict: correct communication infrastructure for mobile computation. POPL 2001: 116-127 - [c12]Peter Sewell
Modules, abstract types, and distributed versioning. POPL 2001: 236-247 - [c11]Andrei Serjantov, Peter Sewell
The UDP Calculus: Rigorous Semantics for Real Networking. TACS 2001: 535-559 - 2000
- [j2]Pawel T. Wojciechowski
Nomadic Pict: language and infrastructure design for mobile agents. IEEE Concurr. 8(2): 42-52 (2000) - [c10]Peter Sewell
Secure Composition of Untrusted Code: Wrappers and Causality Types. CSFW 2000: 269-284 - [c9]Gian Luca Cattani, Peter Sewell
Models for Name-Passing Processes: Interleaving and Causal. LICS 2000: 322-333 - [c8]Peter Sewell:
Preface. HLCL 2000: 17-18 - [e1]John H. Reppy, Peter Sewell:
4th International Workshop on High-Level Concurrent Languages, HLCL 2000, Satellite to PLI 2000, Montreal, Canada, September 20, 2000. Electronic Notes in Theoretical Computer Science 41(2), Elsevier 2000 [contents]
1990 – 1999
- 1999
- [c7]Peter Sewell
Secure Composition of Insecure Components. CSFW 1999: 136-150 - [c6]Pawel T. Wojciechowski
Nomadic Pict: Language and Infrastructure Design for Mobile Agents. ASA/MA 1999: 2-12 - 1998
- [c5]Peter Sewell
From Rewrite to Bisimulation Congruences. CONCUR 1998: 269-284 - [c4]Peter Sewell
Global/Local Subtyping and Capability Inference for a Distributed pi-calculus. ICALP 1998: 695-706 - [c3]Peter Sewell
Location-Independent Communication for Mobile Agents: A Two-Level Architecture. ICCL Workshop: Internet Programming Languages 1998: 1-31 - 1997
- [j1]Peter Sewell
Nonaxiomatisability of Equivalences over Finite State Processes. Ann. Pure Appl. Log. 90(1-3): 163-191 (1997) - [c2]Peter Sewell:
On Implementations and Semantics of a Concurrent Programming Language. CONCUR 1997: 391-405 - 1994
- [c1]Peter Sewell:
Bisimulation is Not Finitely (First Order) Equationally Axiomatisable. LICS 1994: 62-70
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-10 20:52 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: