Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Peter Sewell

Peter Sewell

Professor of Computer Science and EPSRC Leadership Fellow, Computer Laboratory, University of Cambridge
Member of the Cambridge Programming, Logic, and Semantics Group
Fellow of Wolfson college

Here are my contact details, a photo, short bio, and CV

News

Mark Batty won the 2015 SIGPLAN John C. Reynolds Doctoral Dissertation award for his thesis The C11 and C++11 Concurrency Model.

Teaching

Research

My research aims to put the engineering of real-world computer systems on better foundations, developing techniques (both mathematically rigorous and pragmatically useful) to make systems that are better-understood, more robust, and more secure. This applied semantics needs tightly integrated theoretical and practical research, spanning a range of Computer Science: I work in architectural description, programming languages, networking, and security, developing and using techniques from semantics, type systems, automated reasoning, and concurrency theory.

Research Projects

REMS: Rigorous Engineering for Mainstream Systems

Research Topics

I also maintain a page of Action Calculi links.

Recent Papers (with Previous Papers and bibtex data)

Into the Depths of C: Elaborating the De Facto Standards. Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson, and Peter Sewell. In Proc. 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '16). Distinguished paper award. (more details).
An operational semantics for C/C++11 concurrency. Kyndylan Nienhuis, Kayvan Memarian, Peter Sewell. Draft.
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. Jean Pichon-Pharabod and Peter Sewell. In POPL 2016. (more details).
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. In POPL 2016 (more details).
An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. Kathryn E. Gray, Gabriel Kerneis, Dominic Mulligan, Christopher Pulte, Susmit Sarkar, Peter Sewell. In MICRO-48, 2015.
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. T. Ridge, D. Sheets, T. Tuerk, A. Madhavapeddy, A. Giugliano, P. Sewell. In SOSP 2015. More details at sibylfs.io.
Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation. David Kaloper-Mersinjak, Hannes Mehnert, Anil Madhavapeddy, Peter Sewell. In USENIX Security 2015. More details at nqsb.io.
The Problem of Programming Language Concurrency Semantics. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, Peter Sewell. In ESOP 2015
Lem: reusable engineering of real-world semantics. Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. In ICFP 2014.
POPL 2014 PC Chair Report. Peter Sewell. In ACM SIGPLAN Notices.
Engineering with Logic: Rigorous Specification and Validation for TCP/IP and the Sockets API. Steve Bishop, Matthew Fairbairn, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, Keith Wansbrough. Draft.
A Tutorial Introduction to the ARM and POWER Relaxed Memory Models. Luc Maranget, Susmit Sarkar, and Peter Sewell. Draft.
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell. In J.ACM. (more details)
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. In CAV 2012. (more details)
Synchronising C/C++ and POWER. Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, Derek Williams. In PLDI 2012. (more details)
Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER. Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell. In POPL 2012. (more details)
Understanding POWER Multiprocessors. Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams. In PLDI 2011 (more details)
Litmus: Running Tests Against Hardware. Jade Alglave, Luc Maranget, Susmit Sarkar and Peter Sewell. Tool Demonstration Paper. In TACAS 2011.
Relaxed-Memory Concurrency and Verified Compilation. Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell. In POPL 2011 (more details)
Mathematizing C++ Concurrency. Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. In POPL 2011 (more details)
x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen. In Communications of the ACM (Research Highlights) 2010 No.7.

Funding

REMS: Rigorous Engineering for Mainstream Systems. EPSRC Programme Grant EP/K008528/1, 2013-2019.
Semantic Foundations for Real-World Systems. EPSRC Leadership Fellowship EP/H005633/1. 2009-2014.
ARM Architectural Semantics EPSRC/ARM Industrial CASE PhD studentship, 2014
...previous funding

Meetings

ITP 2014: Conference on Interactive Theorem Proving (invited speaker)
CHLLP 2014: Workshop on Certification of high-level and low-level programs (in the Institut Henri Poincare thematic trimester on Semantics of proofs and certified mathematics, 2014 (invited speaker)
PLMW 2014: SIGPLAN Programming Languages Mentoring Workshop (invited speaker)
POPL 2014 (PC chair)
PiP 2014: first workshop on Principles in Practice, co-located with POPL 2014 (co-chair)
CPP: the 3rd international conference on Certified Programs and Proofs, 2013 (PC)
SLS 2013: Microsoft Research Workshop on Scalable Language Specification, (invited speaker)
VCP 2013: Microsoft Research Workshop on Verified Concurrent Programmes: Theory, Tools and Experiments, (invited speaker)
Linux Collaboration Summit, 2013 (invited speaker)
SRC/NSF/CCC Workshop on Convergence of Software Assurance Methodologies and Trustworthy Semiconductor Design and Manufacture (SA+TS), 2013 (invited speaker)
PLMW 2013: SIGPLAN Programming Languages Mentoring Workshop (invited speaker)
POPL 2013 (PC)
ICFP 2012 (invited speaker)
CONCUR 2012 (invited speaker)
Microsoft Cambridge PhD School 2012, TRANSFORM (invited speaker)
Milner Symposium, 2012 (invited speaker)
...previous meetings

People

Some Coauthors

Jade Alglave Mair Allen-Williams Peter Boehm Gavin Bierman Adam Biltcliffe Steve Bishop Gian Luca Cattani Michael Dales Mike Dodds Matthew Fairbairn Pierre Habouzit Michael Hicks Sam Jansen James Leifer Sela Mador-Haim Luc Maranget Michael Norrish Scott Owens Gilles Peskine Benjamin Pierce Tom Ridge Susmit Sarkar Jaroslav Sevcik Mark Shinwell Michael Smith Thomas Tuerk Viktor Vafeiadis Jan Vitek Keith Wansbrough Stephanie Weirich Francesco Zappa Nardelli Steve Zdancewic

Current RAs

PhD Students

David Kaloper Meršinjak 2016-. (supervised jointly with Anil Madhavapeddy)
Christopher Pulte 2014-.
Jean Pichon-Pharabod 2013-.
Shaked Flur 2013-.
Kyndylan Nienhuis 2013-.
Justus Matthiesen 2012-. (supervised jointly with Andrew Pitts)
Kayvan Memarian 2011-.
Mark Batty 2009-2014. The C11 and C++11 Concurrency Model. Winner of the 2015 SIGPLAN John C. Reynolds Doctoral Dissertation award and the BCS 2015 Distinguished Dissertation award.
Rok Strniša 2005-2010. Formalising, improving, and reusing the Java Module System
John Billings 05-. Switched to work on Metarouting with Tim Griffin.
Gareth Stoyle 2001-2006. Dynamic Software Updating
Moritz Becker 2001-2005. Distributed trust management, applied to electronic health records.
Andrei Serjantov -2004. On the Anonymity of Anonymity Systems
Asis Unyapoth -2001. Nomadic Pi Calculi: Expressing and Verifying Infrastructure for Mobile Computation
Pawel Wojciechowski -2000. Nomadic Pict: Language and Infrastructure Design for Mobile Computation

Other

Linepithema humile

Some tangible things

Electric orrery and mirrored-pinhole heliostat

Litmus Test shop

[Validate this page.]