Associate Professor at the University of Oxford,
Royal Society University Research Fellow,
Tutorial Fellow at Mansfield College.
Research Interests. My research interests are in programming language semantics, type systems, concurrency, and verification. My research focuses on systems software, low-level software such as operating systems and hypervisors, whose correctness and security is critical for the overall computer system but which is especially difficult to reason about formally or informally. My past research focused on establishing precise mathematical models of the hardware architectures systems software runs on – especially the relaxed concurrency behaviour of ARM and RISC-V. Now my main research focus is correctness proof of systems software using separation logic. The goal of my Royal Society University Research Fellowship is to build reasoning principles for systems software at the abstraction level of the programming language, sound with respect to systems software’s low-level manipulation of architectural state and the hardware’s relaxed semantics.
Bio. Before joining Oxford I was a Senior Research Associate and Affiliated Lecturer in Computer Science at the University of Cambridge, following a PhD in Cambridge supervised by Peter Sewell.
christopher.pulte@cs.ox.ac.uk
Department of Computer Science
University of Oxford
Wolfson Building
Parks Road
Oxford OX1 3QD
Fulminate: Testing CN Separation-Logic Specifications in C. Rini Banerjee, Kayvan Memarian, Dhruv Makwana, Christopher Pulte, Neel Krishnaswami, and Peter Sewell, in POPL 2025. (paper)
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version). Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell, in Formal Methods in System Design (May 2023). (paper)
CN: Verifying Systems C Code with Separation-Logic Refinement Types. Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami, in POPL 2023. (project, paper)
Relaxed virtual memory in Armv8-A. Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell, in ESOP 2022. (project, paper, extended version)
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models. Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell, in CAV 2021. (paper, extended version)
Repairing and Mechanising the JavaScript Relaxed Memory Model. Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, Shu-yu Guo, in PLDI 2020. (paper)
ARMv8-A system semantics: instruction fetch in relaxed architectures. Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell, in ESOP 2020. (project, paper, extended version)
Promising-ARM/RISC-V: a simpler and faster operational concurrency model. Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur, in PLDI 2019. (project, paper)
The Semantics of Multicopy Atomic ARMv8 and RISC-V. Christopher Pulte, PhD Thesis. 2018. (Cambridge repository)
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, in POPL 2019. (project, paper)
The RISC-V Instruction Set Manual Volume I: Unprivileged ISA. A. Waterman and K. Asanović, editors. December 2018. Document Version 20181221-Public-Review-draft. Contributors: Arvind, K. Asanović, R. Avižienis, J. Bachmeyer, C. F. Batten, A. J. Baum, A. Bradbury, S. Beamer, P. Briggs, C. Celio, C. Chang, D. Chisnall, P. Clayton, P. Dabbelt, R. Espasa, S. Flur, S. Freudenberger, J. Gray, M. Hamburg, J. Hauser, D. Horner, B. Hoult, A. Joannou, O. Johansson, B. Keller, Y. Lee, P. Loewenstein, D. Lustig, Y. Manerkar, L. Maranget, M. Martonosi, J. Myers, V. Nagarajan, R. Nikhil, J. Oberhauser, S. O’Rear, A. Ou, J. Ousterhout, D. Patterson, C. Pulte, J. Renau, C. Schmidt, P. Sewell, S. Sarkar, M. Taylor, W. Terpstra, M. Thomas, T. Thorn, C. Trippel, R. VanDeWalker, M. Vijayaraghavan, M. Wachs, A. Waterman, R. Watson, D. Williams, A. Wright, R. Zandijk, S. Zhang. (document)
Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell, in POPL 2018. (project, paper)
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, in POPL 2017. (project, paper)
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. (project, paper)
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, in MICRO 2015. (paper)
Imperative Programming: Computer Science Preliminary Examinations, in 2025/26.
Hoare Logic and Model Checking: CS Part II, in 2021/22-2024/25.
Guest lecturing on Peter Sewell and Tim Harris’s Multicore Semantics and Programming: ACS MPhil and CS Part II, in 2019/20 – 2024/25.
CN, a separation logic refinement type system for C, based on the Cerberus C semantics: we translate C to Core using Cerberus and type-check the Core. Refinement typing is handled using an SMT solver.
rmem is a tool for executable formal semantics of relaxed memory architectures, including ARMv8 and RISC-V. The rmem tool can also be tried in an online interface.