Follow
Christopher Pulte
Christopher Pulte
Verified email at cam.ac.uk - Homepage
Title
Cited by
Cited by
Year
Modelling the ARMv8 architecture, operationally: Concurrency and ISA
S Flur, KE Gray, C Pulte, S Sarkar, A Sezgin, L Maranget, W Deacon, ...
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2016
1812016
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8
C Pulte, S Flur, W Deacon, J French, S Sarkar, P Sewell
Proceedings of the ACM on Programming Languages 2 (POPL), 1-29, 2017
1672017
ISA Semantics for ARMv8-a, RISC-v, and CHERI-MIPS
A Armstrong, T Bauereiss, B Campbell, A Reid, KE Gray, RM Norton, ...
Proceedings of the ACM on Programming Languages 3 (POPL), 1-31, 2019
1462019
An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors
KE Gray, G Kerneis, D Mulligan, C Pulte, S Sarkar, P Sewell
Proceedings of the 48th International Symposium on Microarchitecture, 635-646, 2015
542015
Promising-ARM/RISC-V: a simpler and faster operational concurrency model
C Pulte, J Pichon-Pharabod, J Kang, SH Lee, CK Hur
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019
482019
Mixed-size concurrency: ARM, Power, C/C++ 11, and SC
S Flur, S Sarkar, C Pulte, K Nienhuis, L Maranget, KE Gray, A Sezgin, ...
ACM SIGPLAN Notices 52 (1), 429-442, 2017
482017
Repairing and mechanising the JavaScript relaxed memory model
C Watt, C Pulte, A Podkopaev, G Barbier, S Dolan, S Flur, ...
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language …, 2020
212020
Isla: Integrating full-scale ISA semantics and axiomatic concurrency models
A Armstrong, B Campbell, B Simner, C Pulte, P Sewell
Computer Aided Verification: 33rd International Conference, CAV 2021 …, 2021
192021
ARMv8-A system semantics: instruction fetch in relaxed architectures
B Simner, S Flur, C Pulte, A Armstrong, J Pichon-Pharabod, L Maranget, ...
Programming Languages and Systems: 29th European Symposium on Programming …, 2020
182020
Detailed models of instruction set architectures: From pseudocode to formal semantics
A Armstrong, T Bauereiss, B Campbell, S Flur, KE Gray, P Mundkur, ...
Proceedings of the 25th Automated Reasoning Workshop: Bridging the Gap …, 2018
122018
Relaxed virtual memory in Armv8-A
B Simner, A Armstrong, J Pichon-Pharabod, C Pulte, R Grisenthwaite, ...
European Symposium on Programming, 143-173, 2022
112022
The semantics of multicopy atomic ARMv8 and RISC-V
C Pulte
University of Cambridge, 2019
92019
The Sail instruction-set semantics specification language
KE Gray, P Sewell, C Pulte, S Flur, R Norton-Wright
Technical report published by Cambridge University, 2017
82017
CN: Verifying systems C code with separation-logic refinement types
C Pulte, DC Makwana, T Sewell, K Memarian, P Sewell, N Krishnaswami
Proceedings of the ACM on Programming Languages 7 (POPL), 1-32, 2023
62023
The state of sail
A Armstrong, T Bauereiss, B Campbell, A Reid, KE Gray, R Norton, ...
SpISA 2019: Workshop on Instruction Set Architecture Specification, 2019
42019
Sail
A Armstrong, T Bauereiss, B Campbell, S Gray, G Kerneis, ...
32019
The Sail instruction-set semantics specification language
A Armstrong, T Bauereiss, B Campbell, KE Gray, R Norton-Wright, C Pulte, ...
22021
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)
A Armstrong, B Campbell, B Simner, C Pulte, P Sewell
Formal Methods in System Design, 1-24, 2023
12023
Relaxed virtual memory in Armv8-A (extended version)
B Simner, A Armstrong, J Pichon-Pharabod, C Pulte, R Grisenthwaite, ...
arXiv preprint arXiv:2203.00642, 2022
2022
Research data supporting “Mixed-size Concurrency: ARM, POWER, C/C++ 11, and SC”
S Flur, S Sarkar, C Pulte, K Nienhuis, L Maranget, KE Gray, A Sezgin, ...
University of Cambridge, 2016
2016
The system can't perform the operation now. Try again later.
Articles 1–20