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
Researcher and Research Engineer Positions in Rigorous Engineering
for Mainstream Systems (REMS)
Applications are invited for several postdoctoral researcher and postgraduate
research engineer positions: see REMS for details.
PhD CASE Studentship on ARM architectural semantics
Applications are invited for a fully funded PhD CASE studentship at
the University of Cambridge Computer Laboratory, with industrial
sponsorship from ARM Ltd; here are more details.
My research aims to put the engineering of real-world computer
systems on solid foundations, developing techniques -both
mathematically rigorous and pragmatically useful-
to enable the
construction of systems that are better-understood, more robust, and
more secure.
To do this requires tightly integrated theoretical and practical
research, spanning a range of Computer Science.
This is, broadly, applied semantics: I work in
programming languages, networking, and security,
developing and using techniques from
semantics, type systems, automated reasoning, and concurrency theory.
Relaxed memory models must be
rigorous. In EC^2.
Francesco Zappa Nardelli, Peter Sewell, Jaroslav Sevcik, Susmit
Sarkar, Scott Owens, Luc Maranget, Mark Batty, and Jade Alglave
The Semantics of Power and ARM Multiprocessor
Machine Code
(in DAMP
2009).
Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit
Sarkar, Peter Sewell, and Francesco Zappa Nardelli. Note that the
model presented here has some major flaws; further work is in
progress.