| 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 | 202 | 2016 |
| 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 | 195 | 2017 |
| 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 | 182 | 2019 |
| 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 | 66 | 2015 |
| 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 | 65 | 2019 |
| 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 | 61 | 2017 |
| 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 | 31 | 2020 |
| 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 | 27 | 2021 |
| 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 | 25 | 2020 |
| 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 | 24 | 2023 |
| Relaxed virtual memory in Armv8-A B Simner, A Armstrong, J Pichon-Pharabod, C Pulte, R Grisenthwaite, ... European Symposium on Programming, 143-173, 2022 | 22 | 2022 |
| The semantics of multicopy atomic ARMv8 and RISC-V C Pulte | 13 | 2019 |
| 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 Automated Reasoning Workshop, 2018 | 12 | 2018 |
| The Sail instruction-set semantics specification language KE Gray, P Sewell, C Pulte, S Flur, R Norton-Wright Technical report, Cambridge University, 2017. 86 BIBLIOGRAPHY, 2017 | 10 | 2017 |
| 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 63 (1), 110-133, 2024 | 4 | 2024 |
| 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 | 4 | 2019 |
| The Sail instruction-set semantics specification language A Armstrong, T Bauereiss, B Campbell, KE Gray, R Norton-Wright, C Pulte, ... | 3 | 2021 |
| Fulminate: Testing CN Separation-Logic Specifications in C R Banerjee, K Memarian, D Makwana, C Pulte, N Krishnaswami, P Sewell Proceedings of the ACM on Programming Languages 9 (POPL), 1260-1292, 2025 | | 2025 |
| 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 |
