Christopher Pulte

16 papers A* 5A 2Journal 7Unranked 1
YearRankTypeTitle / Venue / Authors
2025 J jnl
Fulminate: Testing CN Separation-Logic Specifications in C.
Proc. ACM Program. Lang.
Rini Banerjee, Kayvan Memarian, Dhruv C. Makwana, Christopher Pulte, Neel Krishnaswami, Peter Sewell
2024 J jnl
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version).
Formal Methods Syst. Des.
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
2023 J jnl
CN: Verifying Systems C Code with Separation-Logic Refinement Types.
Proc. ACM Program. Lang.
Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami
2022 J jnl
Relaxed virtual memory in Armv8-A (extended version).
CoRR
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell
2022 A conf
Relaxed virtual memory in Armv8-A.
ESOP
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell
2021 — conf
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models.
CAV (1)
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
2020 A conf
ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures.
ESOP
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell
2020 J jnl
Repairing and Mechanising the JavaScript Relaxed Memory Model.
CoRR
Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, Shu-Yu Guo
2020 A* conf
Repairing and mechanising the JavaScript relaxed memory model.
PLDI
Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, Shu-Yu Guo
2019 J jnl
ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS.
Proc. ACM Program. Lang.
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
2019 A* conf
Promising-ARM/RISC-V: a simpler and faster operational concurrency model.
PLDI
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, Chung-Kil Hur
2019 — —
The semantics of multicopy atomic ARMv8 and RISC-V
Christopher Pulte
2018 J jnl
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8.
Proc. ACM Program. Lang.
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, Peter Sewell
2017 A* conf
Mixed-size concurrency: ARM, POWER, C/C++11, and SC.
POPL
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, Peter Sewell
2016 A* conf
Modelling the ARMv8 architecture, operationally: concurrency and ISA.
POPL
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell
2015 A* conf
An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors.
MICRO
Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, Peter Sewell